diff -r 48c2eb84d5ce -r c0eac04ae3b4 Nominal/ExPS3.thy
--- a/Nominal/ExPS3.thy	Sat Apr 03 21:53:04 2010 +0200
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,38 +0,0 @@
-theory ExPS3
-imports "Parser"
-begin
-
-(* example 3 from Peter Sewell's bestiary *)
-
-atom_decl name
-
-ML {* val _ = recursive := false  *}
-nominal_datatype exp =
-  VarP "name"
-| AppP "exp" "exp"
-| LamP x::"name" e::"exp" bind x in e
-| LetP x::"name" p::"pat3" e1::"exp" e2::"exp" bind x in e2, bind "bp p" in e1
-and pat3 =
-  PVar "name"
-| PUnit
-| PPair "pat3" "pat3"
-binder
-  bp :: "pat3 \<Rightarrow> atom set"
-where
-  "bp (PVar x) = {atom x}"
-| "bp (PUnit) = {}"
-| "bp (PPair p1 p2) = bp p1 \<union> bp p2"
-
-thm exp_pat3.fv
-thm exp_pat3.eq_iff
-thm exp_pat3.bn
-thm exp_pat3.perm
-thm exp_pat3.induct
-thm exp_pat3.distinct
-thm exp_pat3.fv
-thm exp_pat3.supp
-
-end
-
-
-