--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/Nominal/Ex1rec.thy	Tue Mar 23 08:42:02 2010 +0100
@@ -0,0 +1,33 @@
+theory Ex1rec
+imports "Parser" "../Attic/Prove"
+begin
+
+atom_decl name
+
+ML {* val _ = recursive := true *}
+nominal_datatype lam' =
+  VAR' "name"
+| APP' "lam'" "lam'"
+| LAM' x::"name" t::"lam'"  bind x in t
+| LET' bp::"bp'" t::"lam'"   bind "bi' bp" in t
+and bp' =
+  BP' "name" "lam'"
+binder
+  bi'::"bp' \<Rightarrow> atom set"
+where
+  "bi' (BP' x t) = {atom x}"
+
+thm lam'_bp'.fv
+thm lam'_bp'.eq_iff[no_vars]
+thm lam'_bp'.bn
+thm lam'_bp'.perm
+thm lam'_bp'.induct
+thm lam'_bp'.inducts
+thm lam'_bp'.distinct
+ML {* Sign.of_sort @{theory} (@{typ lam'}, @{sort fs}) *}
+thm lam'_bp'.fv[simplified lam'_bp'.supp]
+
+end
+
+
+