--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/Nominal/Ex2.thy	Tue Mar 23 08:42:02 2010 +0100
@@ -0,0 +1,37 @@
+theory Ex2
+imports "Parser"
+begin
+
+text {* example 2 *}
+
+atom_decl name
+
+ML {* val _ = recursive := false  *}
+nominal_datatype trm' =
+  Var "name"
+| App "trm'" "trm'"
+| Lam x::"name" t::"trm'"          bind x in t
+| Let p::"pat'" "trm'" t::"trm'"   bind "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'.fv
+thm trm'_pat'.eq_iff
+thm trm'_pat'.bn
+thm trm'_pat'.perm
+thm trm'_pat'.induct
+thm trm'_pat'.distinct
+thm trm'_pat'.fv[simplified trm'_pat'.supp]
+
+end
+
+
+