--- a/Nominal/ExPS6.thy	Sat Apr 03 21:53:04 2010 +0200
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,39 +0,0 @@
-theory ExPS6
-imports "Parser"
-begin
-
-(* example 6 from Peter Sewell's bestiary *)
-
-atom_decl name
-
-(* The binding structure is too complicated, so equivalence the
-   way we define it is not true *)
-
-ML {* val _ = recursive := false  *}
-nominal_datatype exp6 =
-  EVar name
-| EPair exp6 exp6
-| ELetRec x::name p::pat6 e1::exp6 e2::exp6 bind x in e1, bind x in e2, bind "bp6 p" in e1
-and pat6 =
-  PVar' name
-| PUnit'
-| PPair' pat6 pat6
-binder
-  bp6 :: "pat6 \<Rightarrow> atom set"
-where
-  "bp6 (PVar' x) = {atom x}"
-| "bp6 (PUnit') = {}"
-| "bp6 (PPair' p1 p2) = bp6 p1 \<union> bp6 p2"
-
-thm exp6_pat6.fv
-thm exp6_pat6.eq_iff
-thm exp6_pat6.bn
-thm exp6_pat6.perm
-thm exp6_pat6.induct
-thm exp6_pat6.distinct
-thm exp6_pat6.supp
-
-end
-
-
-