--- a/src/HOL/List.thy Thu Sep 20 16:37:28 2007 +0200
+++ b/src/HOL/List.thy Thu Sep 20 16:37:29 2007 +0200
@@ -215,18 +215,23 @@
text{* The following simple sort functions are intended for proofs,
not for efficient implementations. *}
-fun (in linorder) sorted :: "'a list \<Rightarrow> bool" where
-"sorted [] \<longleftrightarrow> True" |
-"sorted [x] \<longleftrightarrow> True" |
-"sorted (x#y#zs) \<longleftrightarrow> x \<^loc><= y \<and> sorted (y#zs)"
-
-fun (in linorder) insort :: "'a \<Rightarrow> 'a list \<Rightarrow> 'a list" where
-"insort x [] = [x]" |
-"insort x (y#ys) = (if x \<^loc><= y then (x#y#ys) else y#(insort x ys))"
-
-fun (in linorder) sort :: "'a list \<Rightarrow> 'a list" where
-"sort [] = []" |
-"sort (x#xs) = insort x (sort xs)"
+context linorder
+begin
+
+fun sorted :: "'a list \<Rightarrow> bool" where
+ "sorted [] \<longleftrightarrow> True" |
+ "sorted [x] \<longleftrightarrow> True" |
+ "sorted (x#y#zs) \<longleftrightarrow> x \<^loc><= y \<and> sorted (y#zs)"
+
+fun insort :: "'a \<Rightarrow> 'a list \<Rightarrow> 'a list" where
+ "insort x [] = [x]" |
+ "insort x (y#ys) = (if x \<^loc><= y then (x#y#ys) else y#(insort x ys))"
+
+fun sort :: "'a list \<Rightarrow> 'a list" where
+ "sort [] = []" |
+ "sort (x#xs) = insort x (sort xs)"
+
+end
subsubsection {* List comprehension *}