# HG changeset patch
# User nipkow
# Date 1516529047 -3600
# Node ID f261aefbe702c7741db850c74feb9a9c912bd80a
# Parent  31d04ba288938f551a45b0dc017a45036fcd4308
made sorted fun again

diff -r 31d04ba28893 -r f261aefbe702 src/HOL/List.thy
--- a/src/HOL/List.thy	Sat Jan 20 16:15:05 2018 +0100
+++ b/src/HOL/List.thy	Sun Jan 21 11:04:07 2018 +0100
@@ -360,26 +360,6 @@
 
 context linorder
 begin
-(*
-inductive sorted :: "'a list \<Rightarrow> bool" where
-  Nil [iff]: "sorted []"
-| Cons: "\<forall>y\<in>set xs. x \<le> y \<Longrightarrow> sorted xs \<Longrightarrow> sorted (x # xs)"
-
-lemma sorted_single [iff]: "sorted [x]"
-by (rule sorted.Cons) auto
-
-lemma sorted_many: "x \<le> y \<Longrightarrow> sorted (y # zs) \<Longrightarrow> sorted (x # y # zs)"
-by (rule sorted.Cons) (cases "y # zs" rule: sorted.cases, auto)
-
-lemma sorted_many_eq [simp, code]:
-  "sorted (x # y # zs) \<longleftrightarrow> x \<le> y \<and> sorted (y # zs)"
-by (auto intro: sorted_many elim: sorted.cases)
-
-lemma [code]:
-  "sorted [] \<longleftrightarrow> True"
-  "sorted [x] \<longleftrightarrow> True"
-by simp_all
-*)
 
 fun sorted :: "'a list \<Rightarrow> bool" where
 "sorted [] = True" |
diff -r 31d04ba28893 -r f261aefbe702 src/HOL/Predicate_Compile_Examples/Specialisation_Examples.thy
--- a/src/HOL/Predicate_Compile_Examples/Specialisation_Examples.thy	Sat Jan 20 16:15:05 2018 +0100
+++ b/src/HOL/Predicate_Compile_Examples/Specialisation_Examples.thy	Sun Jan 21 11:04:07 2018 +0100
@@ -48,9 +48,22 @@
 
 values "{x. max_of_my_SucP x 6}"
 
-(* Sortedness is now expressed functionally.
 subsection \<open>Sorts\<close>
 
+inductive sorted :: "'a::linorder list \<Rightarrow> bool" where
+  Nil [simp]: "sorted []"
+| Cons: "\<forall>y\<in>set xs. x \<le> y \<Longrightarrow> sorted xs \<Longrightarrow> sorted (x # xs)"
+
+lemma sorted_single [simp]: "sorted [x]"
+by (rule sorted.Cons) auto
+
+lemma sorted_many: "x \<le> y \<Longrightarrow> sorted (y # zs) \<Longrightarrow> sorted (x # y # zs)"
+by (rule sorted.Cons) (cases "y # zs" rule: sorted.cases, auto)
+
+lemma sorted_many_eq [simp]:
+  "sorted (x # y # zs) \<longleftrightarrow> x \<le> y \<and> sorted (y # zs)"
+by (auto intro: sorted_many elim: sorted.cases)
+
 declare sorted.Nil [code_pred_intro]
   sorted_single [code_pred_intro]
   sorted_many [code_pred_intro]
@@ -77,7 +90,7 @@
   qed
 qed
 thm sorted.equation
-*)
+
 
 section \<open>Specialisation in POPLmark theory\<close>