Mercurial Mercurial > repos > isabelle / changeset
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | raw | gz | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
making sorted_list_of_set executable
authorbulwahn
Mon, 30 Apr 2012 12:14:53 +0200
changeset 47841 179b5e7c9803
parent 47840 732ea1f08e3f
child 47842 bfc08ce7b7b9
child 47843 4da917ed49b7
making sorted_list_of_set executable
src/HOL/List.thy file | annotate | diff | comparison | revisions 
--- a/src/HOL/List.thy	Mon Apr 30 12:14:51 2012 +0200
+++ b/src/HOL/List.thy	Mon Apr 30 12:14:53 2012 +0200
@@ -4483,7 +4483,7 @@
     \<and> distinct (sorted_list_of_set A)"
   by (induct A rule: finite_induct) (simp_all add: set_insort sorted_insort distinct_insort)
 
-lemma sorted_list_of_set_sort_remdups:
+lemma sorted_list_of_set_sort_remdups [code]:
   "sorted_list_of_set (set xs) = sort (remdups xs)"
 proof -
   interpret comp_fun_commute insort by (fact comp_fun_commute_insort)
isabelle