--- a/Nominal/Ex/Ex2.thy	Wed Aug 25 23:16:42 2010 +0800
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,42 +0,0 @@
-theory Ex2
-imports "../NewParser"
-begin
-
-text {* example 2 *}
-declare [[STEPS = 9]]
-
-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 fv_trm_raw.simps[no_vars] fv_pat_raw.simps[no_vars] fv_f_raw.simps[no_vars] f_raw.simps[no_vars]
-thm alpha_trm_raw_alpha_pat_raw_alpha_f_raw.intros[no_vars]
-
-
-
-
-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
-
-
-