--- a/Nominal/Test.thy	Tue Mar 23 08:51:43 2010 +0100
+++ b/Nominal/Test.thy	Tue Mar 23 09:05:23 2010 +0100
@@ -2,109 +2,13 @@
 imports "Parser"
 begin
 
+(* This file contains only the examples that are not supposed to work yet. *)
+
+
 atom_decl name
 
 ML {* val _ = recursive := false  *}
 
-text {* example 3 from Terms.thy *}
-
-nominal_datatype trm3 =
-  Vr3 "name"
-| Ap3 "trm3" "trm3"
-| Lm3 x::"name" t::"trm3"        bind x in t
-| Lt3 r::"rassigns3" t::"trm3"   bind "bv3 r" in t
-and rassigns3 =
-  ANil
-| ACons "name" "trm3" "rassigns3"
-binder
-  bv3
-where
-  "bv3 ANil = {}"
-| "bv3 (ACons x t as) = {atom x} \<union> (bv3 as)"
-
-thm trm3_rassigns3.fv
-thm trm3_rassigns3.eq_iff
-thm trm3_rassigns3.bn
-thm trm3_rassigns3.perm
-thm trm3_rassigns3.induct
-thm trm3_rassigns3.distinct
-thm trm3_rassigns3.fv[simplified trm3_rassigns3.supp]
-
-(* example 5 from Terms.thy *)
-
-nominal_datatype trm5 =
-  Vr5 "name"
-| Ap5 "trm5" "trm5"
-| Lt5 l::"lts" t::"trm5"  bind "bv5 l" in t
-and lts =
-  Lnil
-| Lcons "name" "trm5" "lts"
-binder
-  bv5
-where
-  "bv5 Lnil = {}"
-| "bv5 (Lcons n t ltl) = {atom n} \<union> (bv5 ltl)"
-
-thm trm5_lts.fv
-thm trm5_lts.eq_iff
-thm trm5_lts.bn
-thm trm5_lts.perm
-thm trm5_lts.induct
-thm trm5_lts.distinct
-thm trm5_lts.fv[simplified trm5_lts.supp]
-
-(* example 3 from Peter Sewell's bestiary *)
-
-nominal_datatype exp =
-  VarP "name"
-| AppP "exp" "exp"
-| LamP x::"name" e::"exp" bind x in e
-| LetP x::"name" p::"pat3" e1::"exp" e2::"exp" bind x in e2, bind "bp'' p" in e1
-and pat3 =
-  PVar "name"
-| PUnit
-| PPair "pat3" "pat3"
-binder
-  bp'' :: "pat3 \<Rightarrow> atom set"
-where
-  "bp'' (PVar x) = {atom x}"
-| "bp'' (PUnit) = {}"
-| "bp'' (PPair p1 p2) = bp'' p1 \<union> bp'' p2"
-
-thm exp_pat3.fv
-thm exp_pat3.eq_iff
-thm exp_pat3.bn
-thm exp_pat3.perm
-thm exp_pat3.induct
-thm exp_pat3.distinct
-thm exp_pat3.fv[simplified exp_pat3.supp]
-
-(* example 6 from Peter Sewell's bestiary *)
-nominal_datatype exp6 =
-  EVar name
-| EPair exp6 exp6
-| ELetRec x::name p::pat6 e1::exp6 e2::exp6 bind x in e1, bind x in e2, bind "bp6 p" in e1
-and pat6 =
-  PVar' name
-| PUnit'
-| PPair' pat6 pat6
-binder
-  bp6 :: "pat6 \<Rightarrow> atom set"
-where
-  "bp6 (PVar' x) = {atom x}"
-| "bp6 (PUnit') = {}"
-| "bp6 (PPair' p1 p2) = bp6 p1 \<union> bp6 p2"
-
-thm exp6_pat6.fv
-thm exp6_pat6.eq_iff
-thm exp6_pat6.bn
-thm exp6_pat6.perm
-thm exp6_pat6.induct
-thm exp6_pat6.distinct
-
-
-(* THE REST ARE NOT SUPPOSED TO WORK YET *)
-
 (* example 7 from Peter Sewell's bestiary *)
 (* dest_Const raised
 nominal_datatype exp7 =
@@ -180,61 +84,6 @@
 thm alpha_trm4_raw_alpha_trm4_raw_list.intros[no_vars]
 thm fv_trm4_raw_fv_trm4_raw_list.simps[no_vars]
 *)
-(* core haskell *)
-atom_decl var
-atom_decl tvar
-
-(* there are types, coercion types and regular types *)
-(* list-data-structure
-nominal_datatype tkind =
-  KStar
-| KFun "tkind" "tkind"
-and ckind =
-  CKEq "ty" "ty"
-and ty =
-  TVar "tvar"
-| TC "string"
-| TApp "ty" "ty"
-| TFun "string" "ty list"
-| TAll tv::"tvar" "tkind" T::"ty"  bind tv in T
-| TEq "ty" "ty" "ty"
-and co =
-  CC "string"
-| CApp "co" "co"
-| CFun "string" "co list"
-| CAll tv::"tvar" "ckind" C::"co"  bind tv in C
-| CEq "co" "co" "co"
-| CSym "co"
-| CCir "co" "co"
-| CLeft "co"
-| CRight "co"
-| CSim "co"
-| CRightc "co"
-| CLeftc "co"
-| CCoe "co" "co"
-
-abbreviation
-  "atoms A \<equiv> atom ` A"
-
-nominal_datatype trm =
-  Var "var"
-| C "string"
-| LAM tv::"tvar" "kind" t::"trm"   bind tv in t
-| APP "trm" "ty"
-| Lam v::"var" "ty" t::"trm"       bind v in t
-| App "trm" "trm"
-| Let x::"var" "ty" "trm" t::"trm" bind x in t
-| Case "trm" "assoc list"
-| Cast "trm" "ty"                   --"ty is supposed to be a coercion type only"
-and assoc =
-  A p::"pat" t::"trm" bind "bv p" in t
-and pat =
-  K "string" "(tvar \<times> kind) list" "(var \<times> ty) list"
-binder
- bv :: "pat \<Rightarrow> atom set"
-where
- "bv (K s ts vs) = (atoms (set (map fst ts))) \<union> (atoms (set (map fst vs)))"
-*)
 
 (* example 8 from Terms.thy *)