--- 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)"