Mercurial Mercurial > repos > isabelle / diff
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | file | latest | revisions | annotate | diff | comparison | raw | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
src/HOL/NumberTheory/IntPrimes.thy
changeset 15229 1eb23f805c06
parent 15003 6145dd7538d7
child 16417 9bc16273c2d4 
--- a/src/HOL/NumberTheory/IntPrimes.thy	Mon Oct 04 15:28:03 2004 +0200
+++ b/src/HOL/NumberTheory/IntPrimes.thy	Tue Oct 05 15:30:50 2004 +0200
@@ -465,7 +465,6 @@
   apply (rule exI)
   apply (rule exI)
   apply (subst xzgcda.simps, auto)
-  apply (simp add: abs_if)
   done
 
 lemma xzgcd_correct_aux2:
@@ -481,7 +480,6 @@
    apply (frule_tac a = "r'" in pos_mod_sign, auto)
   apply (erule_tac P = "xzgcda ?u = ?v" in rev_mp)
   apply (subst xzgcda.simps, auto)
-  apply (simp add: abs_if)
   done
 
 lemma xzgcd_correct:
isabelle