diff -r 48c2eb84d5ce -r c0eac04ae3b4 Nominal/Ex/Test.thy
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/Nominal/Ex/Test.thy	Sat Apr 03 22:31:11 2010 +0200
@@ -0,0 +1,47 @@
+(*<*)
+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
+(*>*)
+
+