--- a/src/HOL/UNITY/Comp.ML Mon May 24 15:44:56 1999 +0200
+++ b/src/HOL/UNITY/Comp.ML Mon May 24 15:45:22 1999 +0200
@@ -8,12 +8,6 @@
From Chandy and Sanders, "Reasoning About Program Composition"
*)
-(*split_all_tac causes a big blow-up*)
-claset_ref() := claset() delSWrapper record_split_name;
-
-Delsimps [split_paired_All];
-
-
(*** component ***)
Goalw [component_def] "SKIP component F";
@@ -54,7 +48,7 @@
Goal "[| F component G; G component F |] ==> F=G";
by (blast_tac (claset() addSIs [program_equalityI,
component_Init, component_Acts]) 1);
-qed "component_anti_sym";
+qed "component_antisym";
Goalw [component_def]
"F component H = (EX G. F Join G = H & Disjoint F G)";