--- a/src/HOLCF/IOA/meta_theory/Sequence.ML Thu Jul 07 19:01:04 2005 +0200
+++ b/src/HOLCF/IOA/meta_theory/Sequence.ML Thu Jul 07 19:18:26 2005 +0200
@@ -304,13 +304,14 @@
Cons_not_UU,Cons_not_less_UU,Cons_not_less_nil,Cons_not_nil];
(* Instead of adding UU_neq_Cons every equation UU~=x could be changed to x~=UU *)
+(*
Goal "UU ~= x>>xs";
by (res_inst_tac [("s1","UU"),("t1","x>>xs")] (sym RS rev_contrapos) 1);
by (REPEAT (Simp_tac 1));
qed"UU_neq_Cons";
Addsimps [UU_neq_Cons];
-
+*)
(* ----------------------------------------------------------------------------------- *)