--- a/Nominal/Ex/Test.thy	Wed Aug 25 23:16:42 2010 +0800
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,40 +0,0 @@
-theory Test
-imports "../NewParser"
-begin
-
-declare [[STEPS = 4]]
-
-atom_decl name
-
-(*
-nominal_datatype trm =
-  Vr "name"
-| Ap "trm" "trm"
-
-thm fv_trm_raw.simps[no_vars]
-*)
-
-(* This file contains only the examples that are not supposed to work yet. *)
-
-
-declare [[STEPS = 2]]
-
-
-(* example 4 from Terms.thy *)
-(* fv_eqvt does not work, we need to repaire defined permute functions
-   defined fv and defined alpha... *)
-(* lists-datastructure does not work yet *)
-
-nominal_datatype trm =
-  Vr "name"
-| Ap "trm" "trm list"
-| Lm x::"name" t::"trm"  bind x in t
-
-(*
-thm alpha_trm4_raw_alpha_trm4_raw_list.intros[no_vars]
-thm fv_trm4_raw_fv_trm4_raw_list.simps[no_vars]
-*)
-
-end
-
-