changeset 68934 | b825fa94fe56 |
parent 68162 | 61878d2aa6c7 |
child 68963 | ed6511997d2b |
--- a/src/HOL/Data_Structures/Sorting.thy Fri Sep 07 20:15:17 2018 +0200 +++ b/src/HOL/Data_Structures/Sorting.thy Fri Sep 07 21:30:55 2018 +0200 @@ -44,7 +44,7 @@ apply(auto simp add: set_insort) done -lemma "sorted (isort xs)" +lemma sorted_isort: "sorted (isort xs)" apply(induction xs) apply(auto simp: sorted_insort) done