src/HOLCF/IOA/meta_theory/ShortExecutions.thy

--- a/src/HOLCF/IOA/meta_theory/ShortExecutions.thy	Tue May 27 14:38:49 1997 +0200
+++ b/src/HOLCF/IOA/meta_theory/ShortExecutions.thy	Tue May 27 15:07:02 1997 +0200
@@ -49,8 +49,8 @@
 
 rules
 
-execThruCut
-  "is_execution_fragment A (s,ex) ==> is_execution_fragment A (s,Cut P ex)"
+Cut_prefixcl_Finite
+  "Finite s ==> (? y. s = Cut P s @@ y)"
 
 LastActExtsmall1
   "LastActExtsch A sch ==> LastActExtsch A (TL`(Dropwhile P`sch))"