--- a/Nominal/ExPS8.thy	Sat Apr 03 21:53:04 2010 +0200
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,56 +0,0 @@
-theory ExPS8
-imports "Parser"
-begin
-
-(* example 8 from Peter Sewell's bestiary *)
-
-atom_decl name
-
-(* One function is recursive and the other one is not,
-   and as the parser cannot handle this we cannot set
-   the reference.  *)
-ML {* val _ = recursive := false  *}
-
-nominal_datatype exp8 =
-  EVar name
-| EUnit
-| EPair exp8 exp8
-| ELetRec l::lrbs8 e::exp8 bind "b_lrbs8 l" in e (* rec *)
-and fnclause =
-  K x::name p::pat8 f::exp8 bind "b_pat p" in f (* non-rec *)
-and fnclauses =
-  S fnclause
-| ORs fnclause fnclauses
-and lrb8 =
-  Clause fnclauses
-and lrbs8 =
-  Single lrb8
-| More lrb8 lrbs8
-and pat8 =
-  PVar name
-| PUnit
-| PPair pat8 pat8
-binder
-  b_lrbs8 :: "lrbs8 \<Rightarrow> atom set" and
-  b_pat :: "pat8 \<Rightarrow> atom set" and
-  b_fnclauses :: "fnclauses \<Rightarrow> atom set" and
-  b_fnclause :: "fnclause \<Rightarrow> atom set" and
-  b_lrb8 :: "lrb8 \<Rightarrow> atom set"
-where
-  "b_lrbs8 (Single l) = b_lrb8 l"
-| "b_lrbs8 (More l ls) = b_lrb8 l \<union> b_lrbs8 ls"
-| "b_pat (PVar x) = {atom x}"
-| "b_pat (PUnit) = {}"
-| "b_pat (PPair p1 p2) = b_pat p1 \<union> b_pat p2"
-| "b_fnclauses (S fc) = (b_fnclause fc)"
-| "b_fnclauses (ORs fc fcs) = (b_fnclause fc) \<union> (b_fnclauses fcs)"
-| "b_lrb8 (Clause fcs) = (b_fnclauses fcs)"
-| "b_fnclause (K x pat exp8) = {atom x}"
-
-thm exp7_lrb_lrbs.eq_iff
-thm exp7_lrb_lrbs.supp
-
-end
-
-
-