equal
deleted
inserted
replaced
463 apply auto |
463 apply auto |
464 done |
464 done |
465 |
465 |
466 lemma r_inverse_ring: "!! a::'a::ring. a dvd 1 ==> a * inverse a = 1" |
466 lemma r_inverse_ring: "!! a::'a::ring. a dvd 1 ==> a * inverse a = 1" |
467 apply (unfold inverse_def dvd_def) |
467 apply (unfold inverse_def dvd_def) |
468 apply (tactic {* asm_full_simp_tac (simpset () delsimprocs [ring_simproc]) 1 *}) |
468 apply (tactic {* asm_full_simp_tac (@{simpset} delsimprocs [ring_simproc]) 1 *}) |
469 apply clarify |
469 apply clarify |
470 apply (rule theI) |
470 apply (rule theI) |
471 apply assumption |
471 apply assumption |
472 apply (rule inverse_unique) |
472 apply (rule inverse_unique) |
473 apply assumption |
473 apply assumption |