--- a/Nominal/TestMorePerm.thy	Sat Apr 03 21:53:04 2010 +0200
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,49 +0,0 @@
-theory TestMorePerm
-imports "Parser"
-begin
-
-(* Since there are more permutations, we do not know how to prove equivalence
-   (it is probably not true with the way alpha is defined now) so *)
-ML {* val _ = cheat_equivp := true *}
-
-
-atom_decl name
-
-(* example from my PHD *)
-
-atom_decl coname
-
-nominal_datatype phd =
-   Ax "name" "coname"
-|  Cut n::"coname" t1::"phd" c::"coname" t2::"phd"              bind n in t1, bind c in t2
-|  AndR c1::"coname" t1::"phd" c2::"coname" t2::"phd" "coname"  bind c1 in t1, bind c2 in t2
-|  AndL1 n::"name" t::"phd" "name"                              bind n in t
-|  AndL2 n::"name" t::"phd" "name"                              bind n in t
-|  ImpL c::"coname" t1::"phd" n::"name" t2::"phd" "name"        bind c in t1, bind n in t2
-|  ImpR c::"coname" n::"name" t::"phd" "coname"                 bind n in t, bind c in t
-
-thm phd.fv
-thm phd.eq_iff
-thm phd.bn
-thm phd.perm
-thm phd.induct
-thm phd.distinct
-thm phd.fv[simplified phd.supp]
-
-text {* weirdo example from Peter Sewell's bestiary *}
-
-nominal_datatype weird =
-  WBind x::"name" y::"name" p1::"weird" p2::"weird" p3::"weird"
-    bind x in p1, bind x in p2, bind y in p2, bind y in p3
-| WV "name"
-| WP "weird" "weird"
-
-thm permute_weird_raw.simps[no_vars]
-thm alpha_weird_raw.intros[no_vars]
-thm fv_weird_raw.simps[no_vars]
-
-
-end
-
-
-