# HG changeset patch
# User nipkow
# Date 1525807570 -7200
# Node ID 2b18a770911f21a1328cc96fb51cda0104116120
# Parent  7e349d1e3c95be27c152f180bf19d1ef9058bb05# Parent  aedeef5e6858609e241385d79c5627b093446148
merged

diff -r 7e349d1e3c95 -r 2b18a770911f src/HOL/List.thy
--- a/src/HOL/List.thy	Tue May 08 20:26:40 2018 +0200
+++ b/src/HOL/List.thy	Tue May 08 21:26:10 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)