| changeset 10448 | da7d0e28f746 |
| parent 10230 | 5eb935d6cc69 |
| child 10789 | 260fa2c67e3e |
--- a/src/HOL/Algebra/abstract/Ring.ML Fri Nov 10 19:15:14 2000 +0100 +++ b/src/HOL/Algebra/abstract/Ring.ML Fri Nov 10 19:15:38 2000 +0100 @@ -280,9 +280,8 @@ by Auto_tac; qed "inverse_unique"; -Goalw [inverse_def, dvd_def] - "!! a::'a::ring. a dvd <1> ==> a * inverse a = <1>"; -by (Asm_simp_tac 1); +Goal "!! a::'a::ring. a dvd <1> ==> a * inverse a = <1>"; +by (asm_full_simp_tac (simpset () addsimps [inverse_ax, dvd_def]) 1); by (Clarify_tac 1); by (rtac someI 1); by (rtac sym 1);