--- a/Nominal/Ex/Ex3.thy	Wed Aug 25 23:16:42 2010 +0800
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,38 +0,0 @@
-theory Ex3
-imports "../NewParser"
-begin
-
-(* Example 3, identical to example 1 from Terms.thy *)
-
-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 "pat" "pat"
-binder
-  f::"pat \<Rightarrow> atom set"
-where
-  "f PN = {}"
-| "f (PS x) = {atom x}"
-| "f (PD p1 p2) = (f p1) \<union> (f p2)"
-
-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(1-2)]
-
-
-
-end
-
-
-