Mercurial Mercurial > repos > isabelle / diff
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | file | latest | revisions | annotate | diff | comparison | raw | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
src/HOL/List.thy
changeset 54890 cb892d835803
parent 54885 3a478d0a0e87
child 55129 26bd1cba3ab5 
--- a/src/HOL/List.thy	Wed Jan 01 01:05:46 2014 +0100
+++ b/src/HOL/List.thy	Wed Jan 01 01:05:48 2014 +0100
@@ -6133,7 +6133,7 @@
 
 definition "abort_Bleast S P = (LEAST x. x \<in> S \<and> P x)"
 
-code_abort abort_Bleast
+declare [[code abort: abort_Bleast]]
 
 lemma Bleast_code [code]:
  "Bleast (set xs) P = (case filter P (sort xs) of
isabelle