--- a/Nominal/Test.thy	Sat Apr 03 21:53:04 2010 +0200
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,47 +0,0 @@
-(*<*)
-theory Test
-imports "Parser"
-begin
-
-(* This file contains only the examples that are not supposed to work yet. *)
-
-
-atom_decl name
-
-(* 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 trm4 =
-  Vr4 "name"
-| Ap4 "trm4" "trm4 list"
-| Lm4 x::"name" t::"trm4"  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]
-*)
-
-(* example 8 from Terms.thy *)
-
-(* Binding in a term under a bn, needs to fail *)
-(*
-nominal_datatype foo8 =
-  Foo0 "name"
-| Foo1 b::"bar8" f::"foo8" bind "bv8 b" in f --"check fo error if this is called foo"
-and bar8 =
-  Bar0 "name"
-| Bar1 "name" s::"name" b::"bar8" bind s in b
-binder
-  bv8
-where
-  "bv8 (Bar0 x) = {}"
-| "bv8 (Bar1 v x b) = {atom v}"
-*)
-
-(* example 9 from Peter Sewell's bestiary *)
-(* run out of steam at the moment *)
-
-end
-(*>*)
-
-