diff -r f7b68d12a91e -r e2930fa53538 src/HOL/List.thy
--- a/src/HOL/List.thy	Wed Sep 19 15:26:58 2007 +0200
+++ b/src/HOL/List.thy	Wed Sep 19 17:16:40 2007 +0200
@@ -43,11 +43,6 @@
   replicate :: "nat => 'a => 'a list"
   splice :: "'a list \<Rightarrow> 'a list \<Rightarrow> 'a list"
 
-(* has been generalized
-abbreviation
-  upto:: "nat => nat => nat list"  ("(1[_../_])") where
-  "[i..j] == [i..<(Suc j)]"
-*)
 
 nonterminals lupdbinds lupdbind
 
@@ -2512,7 +2507,7 @@
 
 lemma sorted_insort: "sorted (insort x xs) = sorted xs"
 apply (induct xs)
- apply(auto simp:sorted_Cons set_insort not_le less_imp_le)
+ apply(auto simp:sorted_Cons set_insort)
 done
 
 theorem sorted_sort[simp]: "sorted (sort xs)"