--- a/src/HOLCF/IOA/meta_theory/Deadlock.ML Mon Apr 27 16:46:56 1998 +0200
+++ b/src/HOLCF/IOA/meta_theory/Deadlock.ML Mon Apr 27 16:47:50 1998 +0200
@@ -50,7 +50,7 @@
Needs compositionality on schedule level, input-enabledness, compatibility
and distributivity of is_exec_frag over @@
**********************************************************************************)
-Delsplits [expand_if];
+Delsplits [split_if];
goal thy "!! sch. [| a : local A; Finite sch; sch : schedules (A||B); \
\ Filter (%x. x:act A)`(sch @@ a>>nil) : schedules A; compatible A B; input_enabled B |] \
\ ==> (sch @@ a>>nil) : schedules (A||B)";
@@ -83,7 +83,7 @@
by (REPEAT (atac 1));
qed"IOA_deadlock_free";
-Addsplits [expand_if];
+Addsplits [split_if];