# HG changeset patch
# User huffman
# Date 1120756706 -7200
# Node ID d0b61beefa495c6a382e4ee655adb078b43e37cb
# Parent  21dbff595bf6323b1eba6773505f15c98b1e2786
fixes to work with UU_reorient_simproc

diff -r 21dbff595bf6 -r d0b61beefa49 src/HOLCF/IOA/meta_theory/Seq.ML
--- a/src/HOLCF/IOA/meta_theory/Seq.ML	Thu Jul 07 19:01:04 2005 +0200
+++ b/src/HOLCF/IOA/meta_theory/Seq.ML	Thu Jul 07 19:18:26 2005 +0200
@@ -1,19 +1,20 @@
 (*  Title:      HOLCF/IOA/meta_theory/Seq.ML
     ID:         $Id$
-    Author:     Olaf Müller
+    Author:     Olaf Mller
 *)  
 
 Addsimps (sfinite.intrs @ seq.rews);
 
 
 (* Instead of adding UU_neq_nil every equation UU~=x could be changed to x~=UU *)
+(*
 Goal "UU ~=nil";
 by (res_inst_tac [("s1","UU"),("t1","nil")]  (sym RS rev_contrapos) 1);
 by (REPEAT (Simp_tac 1));
 qed"UU_neq_nil";
 
 Addsimps [UU_neq_nil];
-
+*)
 
 
 
diff -r 21dbff595bf6 -r d0b61beefa49 src/HOLCF/IOA/meta_theory/Sequence.ML
--- 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];
-
+*)
 
 (* ----------------------------------------------------------------------------------- *)
 
diff -r 21dbff595bf6 -r d0b61beefa49 src/HOLCF/IOA/meta_theory/ShortExecutions.ML
--- a/src/HOLCF/IOA/meta_theory/ShortExecutions.ML	Thu Jul 07 19:01:04 2005 +0200
+++ b/src/HOLCF/IOA/meta_theory/ShortExecutions.ML	Thu Jul 07 19:18:26 2005 +0200
@@ -1,6 +1,6 @@
 (*  Title:      HOLCF/IOA/meta_theory/ShortExecutions.thy
     ID:         $Id$
-    Author:     Olaf Müller
+    Author:     Olaf Mller
 
 Some properties about (Cut ex), defined as follows:
 
@@ -139,7 +139,7 @@
 by (asm_full_simp_tac (simpset() addsimps [Map2Finite]) 1);
 (* csae ~ Finite s *)
 by (asm_full_simp_tac (simpset() addsimps [Cut_UU]) 1);
-by (rtac (Cut_UU RS sym) 1);
+by (rtac (Cut_UU (*RS sym*)) 1);
 by (asm_full_simp_tac (simpset() addsimps [ForallMap,o_def]) 1); 
 by (asm_full_simp_tac (simpset() addsimps [Map2Finite]) 1);
 (* main case *)