--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/Nominal/ExLet.thy	Tue Mar 23 09:05:23 2010 +0100
@@ -0,0 +1,35 @@
+theory ExLet
+imports "Parser"
+begin
+
+text {* example 3 or example 5 from Terms.thy *}
+
+atom_decl name
+
+ML {* val _ = recursive := false  *}
+nominal_datatype trm =
+  Vr "name"
+| Ap "trm" "trm"
+| Lm x::"name" t::"trm"  bind x in t
+| Lt a::"lts" t::"trm"   bind "bv a" in t
+and lts =
+  Nil
+| Cons "name" "trm" "lts"
+binder
+  bn
+where
+  "bn Nil = {}"
+| "bn (Cons x t l) = {atom x} \<union> (bn l)"
+
+thm trm_lts.fv
+thm trm_lts.eq_iff
+thm trm_lts.bn
+thm trm_lts.perm
+thm trm_lts.induct
+thm trm_lts.distinct
+thm trm_lts.fv[simplified trm_lts.supp]
+
+end
+
+
+