# HG changeset patch
# User wenzelm
# Date 1191094784 -7200
# Node ID b448f94b1c882ab6f704b56ad03654e4f5e8f8b5
# Parent  53c1a0a46db3f3f87c8be97ebb0ab35ae19d190b
fixed metis proof (Why did it stop working?);

diff -r 53c1a0a46db3 -r b448f94b1c88 src/HOL/MetisExamples/Message.thy
--- 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
 
 
diff -r 53c1a0a46db3 -r b448f94b1c88 src/HOL/NumberTheory/IntPrimes.thy
--- 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: