
diff -r 6a63a4ce756b -r aedeef5e6858 src/HOL/List.thy
--- 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)




