src/HOLCF/IOA/meta_theory/ShortExecutions.ML

+(*  Title:      HOLCF/IOA/meta_theory/ShortExecutions.thy
+    ID:        
+    Author:     Olaf M"uller
+    Copyright   1997  TU Muenchen
+
+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.
+
+*)