author | wenzelm |
Fri, 07 Sep 2018 23:48:19 +0200 | |
changeset 68937 | cbf5475a0f66 |
parent 68934 | b825fa94fe56 (diff) |
parent 68936 | 90c08c7bab9c (current diff) |
child 68938 | a0b19a163f5e |
child 68941 | c192c8f9f19b |
--- a/src/HOL/Data_Structures/Sorting.thy Fri Sep 07 23:47:26 2018 +0200 +++ b/src/HOL/Data_Structures/Sorting.thy Fri Sep 07 23:48:19 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