diff -r 48c2eb84d5ce -r c0eac04ae3b4 Nominal/Ex2.thy
--- a/Nominal/Ex2.thy	Sat Apr 03 21:53:04 2010 +0200
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,37 +0,0 @@
-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
-
-
-