| changeset 4089 | 96fba19bcbe2 |
| parent 3018 | e65b60b28341 |
| child 4230 | eb5586526bc9 |
--- a/src/HOL/Integ/Group.ML Mon Nov 03 12:12:10 1997 +0100 +++ b/src/HOL/Integ/Group.ML Mon Nov 03 12:13:18 1997 +0100 @@ -70,7 +70,7 @@ by (rtac plus_assoc 2); by (rtac trans 1); by (rtac plus_cong 2); - by (simp_tac (!simpset addsimps [left_inv,left_inv2,right_inv,right_inv2]) 2); + by (simp_tac (simpset() addsimps [left_inv,left_inv2,right_inv,right_inv2]) 2); by (rtac refl 2); by (rtac (zeroL RS sym) 1); qed "inv_plus";