--- a/src/HOL/MetisExamples/Message.thy Sat Sep 29 10:47:05 2007 +0200
+++ b/src/HOL/MetisExamples/Message.thy Sat Sep 29 21:39:44 2007 +0200
@@ -702,7 +702,7 @@
apply (metis MPair_synth UnCI UnE Un_commute Un_upper1 analz.Fst analz_increasing analz_mono insert_absorb insert_subset)
apply (metis MPair_synth UnCI UnE Un_commute Un_upper1 analz.Snd analz_increasing analz_mono insert_absorb insert_subset)
apply (blast intro: analz.Decrypt)
-apply (metis Diff_Int Diff_empty Diff_subset_conv Int_empty_right Un_commute Un_subset_iff Un_upper1 analz_increasing analz_mono synth_increasing)
+apply blast
done
--- a/src/HOL/NumberTheory/IntPrimes.thy Sat Sep 29 10:47:05 2007 +0200
+++ b/src/HOL/NumberTheory/IntPrimes.thy Sat Sep 29 21:39:44 2007 +0200
@@ -416,7 +416,12 @@
z = s and aa = t' and ab = t in xzgcda.induct)
apply (subst zgcd_eq)
apply (subst xzgcda.simps, auto)
- apply (metis abs_of_pos pos_mod_conj simps zgcd_0 zgcd_eq zle_refl zless_le)
+ apply (case_tac "r' mod r = 0")
+ prefer 2
+ apply (frule_tac a = "r'" in pos_mod_sign, auto)
+ apply (rule exI)
+ apply (rule exI)
+ apply (subst xzgcda.simps, auto)
done
lemma xzgcd_correct_aux2: