# HG changeset patch
# User paulson <lp15@cam.ac.uk>
# Date 1391549386 0
# Node ID 3bf50e3cd72716502b6c8408b85e52b551e4fb49
# Parent  eadea363deb66e425e786dcf3bfb94587597ea01
removal of "back", etc.

diff -r eadea363deb6 -r 3bf50e3cd727 src/HOL/Number_Theory/MiscAlgebra.thy
--- a/src/HOL/Number_Theory/MiscAlgebra.thy	Tue Feb 04 21:28:38 2014 +0000
+++ b/src/HOL/Number_Theory/MiscAlgebra.thy	Tue Feb 04 21:29:46 2014 +0000
@@ -239,10 +239,7 @@
   done
 
 lemma (in monoid) inv_eq_one_eq: "x : Units G \<Longrightarrow> (inv x = \<one>) = (x = \<one>)"
-  apply auto
-  apply (subst Units_inv_inv [symmetric])
-  apply auto
-  done
+by (metis Units_inv_inv inv_one)
 
 
 (* This goes in FiniteProduct *)
@@ -281,11 +278,7 @@
 
 lemma (in cring) sum_zero_eq_neg:
     "x : carrier R \<Longrightarrow> y : carrier R \<Longrightarrow> x \<oplus> y = \<zero> \<Longrightarrow> x = \<ominus> y"
-  apply (subgoal_tac "\<ominus> y = \<zero> \<oplus> \<ominus> y")
-  apply (erule ssubst)back
-  apply (erule subst)
-  apply (simp_all add: ring_simprules)
-  done
+by (metis minus_equality)
 
 (* there's a name conflict -- maybe "domain" should be
    "integral_domain" *)
@@ -317,11 +310,7 @@
 
 lemma (in Ring.domain) inv_eq_self: "x : Units R \<Longrightarrow>
     x = inv x \<Longrightarrow> x = \<one> | x = \<ominus> \<one>"
-  apply (rule square_eq_one)
-  apply auto
-  apply (erule ssubst)back
-  apply (erule Units_r_inv)
-  done
+by (metis Units_closed Units_l_inv square_eq_one)
 
 
 (*
@@ -334,7 +323,6 @@
     "finite (carrier R) \<Longrightarrow> finite (Units R)"
   by (rule finite_subset) auto
 
-(* this belongs with MiscAlgebra.thy *)
 lemma (in monoid) units_of_pow:
     "x : Units G \<Longrightarrow> x (^)\<^bsub>units_of G\<^esub> (n::nat) = x (^)\<^bsub>G\<^esub> n"
   apply (induct n)