--- a/Nominal/Ex/TestMorePerm.thy	Wed Aug 25 23:16:42 2010 +0800
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,35 +0,0 @@
-theory TestMorePerm
-imports "../NewParser"
-begin
-
-text {* 
-  "Weirdo" example from Peter Sewell's bestiary. 
-
-  This example is not covered by our binding 
-  specification.
-
-*}
-ML {* val _ = cheat_equivp := true *}
-
-atom_decl name
-
-nominal_datatype weird =
-  Foo_var "name"
-| Foo_pair "weird" "weird" 
-| Foo x::"name" y::"name" p1::"weird" p2::"weird" p3::"weird"
-    bind x in p1 p2, 
-    bind y in p2 p3
-
-thm alpha_weird_raw.intros[no_vars]
-
-thm permute_weird_raw.simps[no_vars]
-thm alpha_weird_raw.intros[no_vars]
-thm fv_weird_raw.simps[no_vars]
-
-equivariance alpha_weird_raw
-
-
-end
-
-
-