--- a/src/HOL/List.thy Tue May 08 15:06:19 2018 +0200
+++ b/src/HOL/List.thy Tue May 08 19:53:29 2018 +0200
@@ -4979,9 +4979,10 @@
text \<open>Sometimes the second equation in the definition of @{const sorted} is to aggressive
because it relates each list element to \emph{all} its successors. Then this equation
-should be removed and \<open>sorted2_simps\<close> should be added instead:\<close>
-
-lemma sorted1: "sorted [x]"
+should be removed and \<open>sorted2_simps\<close> should be added instead.
+Executable code is one such use case.\<close>
+
+lemma sorted1: "sorted [x] = True"
by simp
lemma sorted2: "sorted (x # y # zs) = (x \<le> y \<and> sorted (y # zs))"
@@ -4989,6 +4990,8 @@
lemmas sorted2_simps = sorted1 sorted2
+lemmas [code] = sorted.simps(1) sorted2_simps
+
lemma sorted_tl:
"sorted xs \<Longrightarrow> sorted (tl xs)"
by (cases xs) (simp_all)