--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/Nominal/Ex/LetRec.thy	Thu Aug 26 02:08:00 2010 +0800
@@ -0,0 +1,36 @@
+theory LetRec
+imports "../NewParser"
+begin
+
+declare [[STEPS = 14]]
+
+atom_decl name
+
+nominal_datatype let_rec:
+ lam =
+  Var "name"
+| App "lam" "lam"
+| Lam x::"name" t::"lam"     bind (set) x in t
+| Let_Rec bp::"bp" t::"lam"  bind (set) "bi bp" in bp t
+and bp =
+  Bp "name" "lam"
+binder
+  bi::"bp \<Rightarrow> atom set"
+where
+  "bi (Bp x t) = {atom x}"
+
+thm let_rec.distinct
+thm let_rec.induct
+thm let_rec.exhaust
+thm let_rec.fv_defs
+thm let_rec.bn_defs
+thm let_rec.perm_simps
+thm let_rec.eq_iff
+thm let_rec.fv_bn_eqvt
+thm let_rec.size_eqvt
+
+
+end
+
+
+