# HG changeset patch
# User haftmann
# Date 1207144709 -7200
# Node ID a329af578d69d63bb17dd6f03a52e87e8ad2988d
# Parent  294708d83e83e112e49be8a2b6a533de7dd3ad7e
tuned proof

diff -r 294708d83e83 -r a329af578d69 src/HOL/NumberTheory/Euler.thy
--- a/src/HOL/NumberTheory/Euler.thy	Wed Apr 02 15:58:28 2008 +0200
+++ b/src/HOL/NumberTheory/Euler.thy	Wed Apr 02 15:58:29 2008 +0200
@@ -88,7 +88,7 @@
   apply (auto simp add: MultInvPair_def)
   apply (subgoal_tac "~ (StandardRes p j = StandardRes p (a * MultInv p j))")
   apply auto
-  apply (metis MultInvPair_distinct Pls_def StandardRes_prop2 int_0_less_1 less_Pls_Bit0 number_of_is_id one_is_num_one order_less_trans)
+  apply (metis MultInvPair_distinct Pls_def StandardRes_def aux number_of_is_id one_is_num_one)
   done