# HG changeset patch
# User haftmann
# Date 1192716576 -7200
# Node ID c93a234ccf2bb4cb9cfd7b3cd40716bb1f11b39c
# Parent  aabaab4ad212d9a50b2dd30c493fb66237580d1a
tuned

diff -r aabaab4ad212 -r c93a234ccf2b src/HOL/List.thy
--- a/src/HOL/List.thy	Thu Oct 18 14:30:55 2007 +0200
+++ b/src/HOL/List.thy	Thu Oct 18 16:09:36 2007 +0200
@@ -2655,9 +2655,7 @@
 
 instance int:: finite_intvl_succ
   successor_int_def: "successor == (%i. i+1)"
-apply(intro_classes)
-apply(simp_all add: successor_int_def ord_class.atLeastAtMost[symmetric])
-done
+by intro_classes (simp_all add: successor_int_def)
 
 text{* Now @{term"[i..j::int]"} is defined for integers. *}
 
diff -r aabaab4ad212 -r c93a234ccf2b src/HOL/MetisExamples/BigO.thy
--- a/src/HOL/MetisExamples/BigO.thy	Thu Oct 18 14:30:55 2007 +0200
+++ b/src/HOL/MetisExamples/BigO.thy	Thu Oct 18 16:09:36 2007 +0200
@@ -1145,7 +1145,7 @@
   apply (unfold lesso_def)
   apply (subgoal_tac "(%x. max (f x - g x) 0) = 0")
 (*??Translation of TSTP raised an exception: Type unification failed: Variable ?'X2.0::type not of sort ord*)
-apply (metis bigo_zero ord_class.max)
+apply (metis bigo_zero)
   apply (unfold func_zero)
   apply (rule ext)
   apply (simp split: split_max)