# HG changeset patch
# User wenzelm
# Date 787224365 -3600
# Node ID 9a03ed31ea2fa97a29945b22c630c40f2219d8db
# Parent  c007eba368b784b85b2f0e3c02ceb93051b9c022
added print_theory that prints stored thms;

diff -r c007eba368b7 -r 9a03ed31ea2f src/Pure/Thy/thy_read.ML
--- a/src/Pure/Thy/thy_read.ML	Fri Dec 09 16:44:31 1994 +0100
+++ b/src/Pure/Thy/thy_read.ML	Mon Dec 12 10:26:05 1994 +0100
@@ -47,6 +47,7 @@
                  -> unit
   val get_thm: theory -> string -> thm
   val thms_of: theory -> (string * thm) list
+  val print_theory: theory -> unit
 end;
 
 
@@ -529,4 +530,18 @@
 val thms_of = Symtab.dest o thmtab;
 
 
+(* print theory *)
+
+fun print_thms thy =
+  let
+    val thms = thms_of thy;
+    fun prt_thm (s, th) = Pretty.block [Pretty.str (s ^ ":"), Pretty.brk 1,
+      Pretty.quote (pretty_thm th)];
+  in
+    Pretty.writeln (Pretty.big_list "stored theorems:" (map prt_thm thms))
+  end;
+
+fun print_theory thy = (Drule.print_theory thy; print_thms thy);
+
+
 end;