--- a/Nominal/ExPS7.thy	Sat Apr 03 21:53:04 2010 +0200
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,33 +0,0 @@
-theory ExPS7
-imports "Parser"
-begin
-
-(* example 7 from Peter Sewell's bestiary *)
-
-atom_decl name
-
-ML {* val _ = recursive := true  *}
-nominal_datatype exp7 =
-  EVar name
-| EUnit
-| EPair exp7 exp7
-| ELetRec l::"lrbs" e::"exp7" bind "b7s l" in e
-and lrb =
-  Assign name exp7
-and lrbs =
-  Single lrb
-| More lrb lrbs
-binder
-  b7 :: "lrb \<Rightarrow> atom set" and
-  b7s :: "lrbs \<Rightarrow> atom set"
-where
-  "b7 (Assign x e) = {atom x}"
-| "b7s (Single a) = b7 a"
-| "b7s (More a as) = (b7 a) \<union> (b7s as)"
-thm exp7_lrb_lrbs.eq_iff
-thm exp7_lrb_lrbs.supp
-
-end
-
-
-