--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/Nominal/Ex/LetPat.thy	Thu Aug 26 02:08:00 2010 +0800
@@ -0,0 +1,39 @@
+theory LetPat
+imports "../NewParser"
+begin
+
+declare [[STEPS = 100]]
+
+atom_decl name
+
+nominal_datatype trm =
+  Var "name"
+| App "trm" "trm"
+| Lam x::"name" t::"trm"       bind (set) x in t
+| Let p::"pat" "trm" t::"trm"  bind (set) "f p" in t
+and pat =
+  PN
+| PS "name"
+| PD "name" "name"
+binder
+  f::"pat \<Rightarrow> atom set"
+where
+  "f PN = {}"
+| "f (PD x y) = {atom x, atom y}"
+| "f (PS x) = {atom x}"
+
+thm trm_pat.distinct
+thm trm_pat.induct
+thm trm_pat.exhaust
+thm trm_pat.fv_defs
+thm trm_pat.bn_defs
+thm trm_pat.perm_simps
+thm trm_pat.eq_iff
+thm trm_pat.fv_bn_eqvt
+thm trm_pat.size_eqvt
+
+
+end
+
+
+