--- a/Nominal/Ex/ExLeroy.thy	Sun May 09 12:26:10 2010 +0100
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,79 +0,0 @@
-theory ExLeroy
-imports "../NewParser"
-begin
-
-(* example form Leroy 96 about modules; OTT *)
-
-atom_decl name
-
-nominal_datatype mexp =
-  Acc "path"
-| Stru "body"
-| Funct x::"name" "sexp" m::"mexp"    bind_set x in m
-| FApp "mexp" "path"
-| Ascr "mexp" "sexp"
-and body =
-  Empty
-| Seq c::defn d::"body"     bind_set "cbinders c" in d
-and defn =
-  Type "name" "ty"
-| Dty "name"
-| DStru "name" "mexp"
-| Val "name" "trm"
-and sexp =
-  Sig sbody
-| SFunc "name" "sexp" "sexp"
-and sbody =
-  SEmpty
-| SSeq C::spec D::sbody    bind_set "Cbinders C" in D
-and spec =
-  Type1 "name"
-| Type2 "name" "ty"
-| SStru "name" "sexp"
-| SVal "name" "ty"
-and ty =
-  Tyref1 "name"
-| Tyref2 "path" "ty"
-| Fun "ty" "ty"
-and path =
-  Sref1 "name"
-| Sref2 "path" "name"
-and trm =
-  Tref1 "name"
-| Tref2 "path" "name"
-| Lam' v::"name" "ty" M::"trm"  bind_set v in M
-| App' "trm" "trm"
-| Let' "body" "trm"
-binder
-    cbinders :: "defn \<Rightarrow> atom set"
-and Cbinders :: "spec \<Rightarrow> atom set"
-where
-  "cbinders (Type t T) = {atom t}"
-| "cbinders (Dty t) = {atom t}"
-| "cbinders (DStru x s) = {atom x}"
-| "cbinders (Val v M) = {atom v}"
-| "Cbinders (Type1 t) = {atom t}"
-| "Cbinders (Type2 t T) = {atom t}"
-| "Cbinders (SStru x S) = {atom x}"
-| "Cbinders (SVal v T) = {atom v}"
-
-thm mexp_body_defn_sexp_sbody_spec_ty_path_trm.fv
-thm mexp_body_defn_sexp_sbody_spec_ty_path_trm.eq_iff
-thm mexp_body_defn_sexp_sbody_spec_ty_path_trm.bn
-thm mexp_body_defn_sexp_sbody_spec_ty_path_trm.perm
-thm mexp_body_defn_sexp_sbody_spec_ty_path_trm.induct
-thm mexp_body_defn_sexp_sbody_spec_ty_path_trm.inducts
-thm mexp_body_defn_sexp_sbody_spec_ty_path_trm.distinct
-thm mexp_body_defn_sexp_sbody_spec_ty_path_trm.supp(1-3,5-7,9-10)
-thm mexp_body_defn_sexp_sbody_spec_ty_path_trm.fv[simplified mexp_body_defn_sexp_sbody_spec_ty_path_trm.supp(1-3,5-7,9-10)]
-
-declare permute_mexp_raw_permute_body_raw_permute_defn_raw_permute_sexp_raw_permute_sbody_raw_permute_spec_raw_permute_ty_raw_permute_path_raw_permute_trm_raw.simps[eqvt]
-declare alpha_gen_eqvt[eqvt]
-
-equivariance alpha_trm_raw
-
-
-end
-
-
-