diff -r ac7dff1194e8 -r 3a5ebb2fcdbf Nominal/Ex/ExPS7.thy
--- a/Nominal/Ex/ExPS7.thy	Mon Sep 20 21:52:45 2010 +0800
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,34 +0,0 @@
-theory ExPS7
-imports "../Nominal2"
-begin
-
-(* example 7 from Peter Sewell's bestiary *)
-
-atom_decl name
-
-declare [[STEPS = 31]]
-
-nominal_datatype exp =
-  Var name
-| Unit
-| Pair exp exp
-| LetRec l::"lrbs" e::"exp"  bind (set) "bs l" in l e
-and lrb =
-  Assign name exp
-and lrbs =
-  Single lrb
-| More lrb lrbs
-binder
-  b :: "lrb \<Rightarrow> atom set" and
-  bs :: "lrbs \<Rightarrow> atom set"
-where
-  "b (Assign x e) = {atom x}"
-| "bs (Single a) = b a"
-| "bs (More a as) = (b a) \<union> (bs as)"
-
-
-
-end
-
-
-