src/HOLCF/IOA/meta_theory/ShortExecutions.ML

 (*  Title:      HOLCF/IOA/meta_theory/ShortExecutions.thy
     ID:         $Id$
-    Author:     Olaf Müller
+    Author:     Olaf Mller
 
 Some properties about (Cut ex), defined as follows:
 
 For every execution ex there is another shorter execution (Cut ex) 
 that has the same trace as ex, but its schedule ends with an external action.

 by (rtac (Cut_nil RS sym) 1);
 by (asm_full_simp_tac (simpset() addsimps [ForallMap,o_def]) 1); 
 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 *)
 by (asm_full_simp_tac (simpset() addsimps [Cut_Cons,MapConc,
           ForallMap,FiniteMap1,o_def]) 1);