# HG changeset patch
# User paulson
# Date 927553522 -7200
# Node ID 8103c1fb092d195961b99c76d8a82fb32ebd3187
# Parent  27a2e763daf8f1bcc7a725cf77b2c67963506565
tidied

diff -r 27a2e763daf8 -r 8103c1fb092d src/HOL/UNITY/Comp.ML
--- 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)";