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.
sort BNFs in output
authorblanchet
Fri, 27 Mar 2015 09:56:34 +0100
changeset 59822 f014a2dc0ac8
parent 59821 fd3a7692e083
child 59823 a03696dc3283
sort BNFs in output
src/HOL/Tools/BNF/bnf_def.ML file | annotate | diff | comparison | revisions 
--- a/src/HOL/Tools/BNF/bnf_def.ML	Fri Mar 27 09:52:57 2015 +0100
+++ b/src/HOL/Tools/BNF/bnf_def.ML	Fri Mar 27 09:56:34 2015 +0100
@@ -1609,7 +1609,8 @@
           [Pretty.block [Pretty.str (bdN ^ ":"), Pretty.brk 1,
             Pretty.quote (Syntax.pretty_term ctxt bd)]]);
   in
-    Pretty.big_list "BNFs:" (map pretty_bnf (Symtab.dest (Data.get (Context.Proof ctxt))))
+    Pretty.big_list "Registered bounded natural functors:"
+      (map pretty_bnf (sort_wrt fst (Symtab.dest (Data.get (Context.Proof ctxt)))))
     |> Pretty.writeln
   end;
isabelle