diff -r 48c2eb84d5ce -r c0eac04ae3b4 Nominal/Ex/ExLeroy.thy
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/Nominal/Ex/ExLeroy.thy	Sat Apr 03 22:31:11 2010 +0200
@@ -0,0 +1,74 @@
+theory ExLeroy
+imports "../Parser"
+begin
+
+(* example form Leroy 96 about modules; OTT *)
+
+atom_decl name
+
+ML {* val _ = recursive := false  *}
+nominal_datatype mexp =
+  Acc "path"
+| Stru "body"
+| Funct x::"name" "sexp" m::"mexp"    bind x in m
+| FApp "mexp" "path"
+| Ascr "mexp" "sexp"
+and body =
+  Empty
+| Seq c::defn d::"body"     bind "cbinders c" in d
+and defn =
+  Type "name" "tyty"
+| Dty "name"
+| DStru "name" "mexp"
+| Val "name" "trmtrm"
+and sexp =
+  Sig sbody
+| SFunc "name" "sexp" "sexp"
+and sbody =
+  SEmpty
+| SSeq C::spec D::sbody    bind "Cbinders C" in D
+and spec =
+  Type1 "name"
+| Type2 "name" "tyty"
+| SStru "name" "sexp"
+| SVal "name" "tyty"
+and tyty =
+  Tyref1 "name"
+| Tyref2 "path" "tyty"
+| Fun "tyty" "tyty"
+and path =
+  Sref1 "name"
+| Sref2 "path" "name"
+and trmtrm =
+  Tref1 "name"
+| Tref2 "path" "name"
+| Lam' v::"name" "tyty" M::"trmtrm"  bind v in M
+| App' "trmtrm" "trmtrm"
+| Let' "body" "trmtrm"
+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_tyty_path_trmtrm.fv
+thm mexp_body_defn_sexp_sbody_spec_tyty_path_trmtrm.eq_iff
+thm mexp_body_defn_sexp_sbody_spec_tyty_path_trmtrm.bn
+thm mexp_body_defn_sexp_sbody_spec_tyty_path_trmtrm.perm
+thm mexp_body_defn_sexp_sbody_spec_tyty_path_trmtrm.induct
+thm mexp_body_defn_sexp_sbody_spec_tyty_path_trmtrm.inducts
+thm mexp_body_defn_sexp_sbody_spec_tyty_path_trmtrm.distinct
+thm mexp_body_defn_sexp_sbody_spec_tyty_path_trmtrm.supp
+thm mexp_body_defn_sexp_sbody_spec_tyty_path_trmtrm.fv[simplified mexp_body_defn_sexp_sbody_spec_tyty_path_trmtrm.supp]
+
+end
+
+
+