src/HOL/Algebra/abstract/Ring2.thy
changeset 26342 0f65fa163304
parent 25762 c03e9d04b3e4
child 26480 544cef16045b
     1.1 --- a/src/HOL/Algebra/abstract/Ring2.thy	Wed Mar 19 22:47:39 2008 +0100
     1.2 +++ b/src/HOL/Algebra/abstract/Ring2.thy	Wed Mar 19 22:50:42 2008 +0100
     1.3 @@ -465,7 +465,7 @@
     1.4  
     1.5  lemma r_inverse_ring: "!! a::'a::ring. a dvd 1 ==> a * inverse a = 1"
     1.6    apply (unfold inverse_def dvd_def)
     1.7 -  apply (tactic {* asm_full_simp_tac (simpset () delsimprocs [ring_simproc]) 1 *})
     1.8 +  apply (tactic {* asm_full_simp_tac (@{simpset} delsimprocs [ring_simproc]) 1 *})
     1.9    apply clarify
    1.10    apply (rule theI)
    1.11     apply assumption