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.
no printing of axioms -- too bulky;
authorwenzelm
Tue, 22 Oct 2019 20:59:57 +0200
changeset 70924 15758fced053
parent 70923 98d9b78b7f47
child 70925 525853e4ec80
no printing of axioms -- too bulky;
src/Pure/Isar/proof_display.ML file | annotate | diff | comparison | revisions 
--- a/src/Pure/Isar/proof_display.ML	Tue Oct 22 20:55:13 2019 +0200
+++ b/src/Pure/Isar/proof_display.ML	Tue Oct 22 20:59:57 2019 +0200
@@ -122,8 +122,6 @@
     val log_cnsts = map_filter (fn (c, (ty, NONE)) => SOME (c, ty) | _ => NONE) cnsts;
     val abbrevs = map_filter (fn (c, (ty, SOME t)) => SOME (c, (ty, t)) | _ => NONE) cnsts;
     val cnstrs = Name_Space.markup_entries verbose ctxt const_space constraints;
-
-    val axms = Name_Space.markup_table verbose ctxt (Theory.axiom_table thy);
   in
     Pretty.chunks
      [Pretty.big_list "classes:" (map pretty_classrel clsses),
@@ -134,7 +132,6 @@
       Pretty.big_list "logical consts:" (map (Pretty.block o prt_const) log_cnsts),
       Pretty.big_list "abbreviations:" (map pretty_abbrev abbrevs),
       Pretty.big_list "constraints:" (map (Pretty.block o prt_const) cnstrs),
-      Pretty.big_list "axioms:" (map pretty_axm axms),
       Pretty.block
         (Pretty.breaks (Pretty.str "oracles:" ::
           map Pretty.mark_str (Thm.extern_oracles verbose ctxt)))]
isabelle