src/HOL/UNITY/Comp.ML

 Composition
 
 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";
 by (force_tac (claset() addIs [Join_SKIP_left], simpset()) 1);
 qed "component_SKIP";

 qed "component_Init";
 
 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)";
 by (blast_tac (claset() addSIs [Diff_Disjoint, Join_Diff2]) 1);
 qed "component_eq";