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. *}