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/Pure/Isar/isar_cmd.ML
changeset 20621 29d57880ba00
parent 20574 a10885a269cb
child 20803 ac78eee049ce 
--- a/src/Pure/Isar/isar_cmd.ML	Tue Sep 19 23:15:24 2006 +0200
+++ b/src/Pure/Isar/isar_cmd.ML	Tue Sep 19 23:15:26 2006 +0200
@@ -43,7 +43,7 @@
   val print_drafts: Path.T list -> Toplevel.transition -> Toplevel.transition
   val pretty_setmargin: int -> Toplevel.transition -> Toplevel.transition
   val print_context: Toplevel.transition -> Toplevel.transition
-  val print_theory: Toplevel.transition -> Toplevel.transition
+  val print_theory: bool -> Toplevel.transition -> Toplevel.transition
   val print_syntax: Toplevel.transition -> Toplevel.transition
   val print_theorems: Toplevel.transition -> Toplevel.transition
   val print_locales: Toplevel.transition -> Toplevel.transition
@@ -218,8 +218,8 @@
 
 val print_context = Toplevel.keep Toplevel.print_state_context;
 
-val print_theory = Toplevel.unknown_theory o
-  Toplevel.keep (ProofDisplay.print_theory o Toplevel.theory_of);
+fun print_theory verbose = Toplevel.unknown_theory o
+  Toplevel.keep (ProofDisplay.print_full_theory verbose o Toplevel.theory_of);
 
 val print_syntax = Toplevel.unknown_theory o
   Toplevel.keep (Display.print_syntax o Toplevel.theory_of) o
isabelle