--- a/Nominal/Ex/TestMorePerm.thy	Thu Apr 08 10:25:38 2010 +0200
+++ b/Nominal/Ex/TestMorePerm.thy	Thu Apr 08 11:40:13 2010 +0200
@@ -2,34 +2,6 @@
 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 =