--- a/src/HOL/ex/Comb.ML Thu Sep 26 11:11:22 1996 +0200
+++ b/src/HOL/ex/Comb.ML Thu Sep 26 12:47:47 1996 +0200
@@ -167,13 +167,13 @@
goal Comb.thy "contract^* = parcontract^*";
by (REPEAT
(resolve_tac [equalityI,
- contract_subset_parcontract RS rtrancl_mono,
- parcontract_subset_reduce RS rtrancl_subset_rtrancl] 1));
+ contract_subset_parcontract RS rtrancl_mono,
+ parcontract_subset_reduce RS rtrancl_subset_rtrancl] 1));
qed "reduce_eq_parreduce";
goal Comb.thy "diamond(contract^*)";
by (simp_tac (!simpset addsimps [reduce_eq_parreduce, diamond_rtrancl,
- diamond_parcontract]) 1);
+ diamond_parcontract]) 1);
qed "diamond_reduce";