# HG changeset patch
# User wenzelm
# Date 938029505 -7200
# Node ID 20adf381fb0a7e587958c141b7b374bdd2b0778d
# Parent  80525697a87cb450e72573788f41efe48d99e0e9
added thms_containing;

diff -r 80525697a87c -r 20adf381fb0a src/Pure/Interface/proof_general.ML
--- a/src/Pure/Interface/proof_general.ML	Wed Sep 22 21:04:55 1999 +0200
+++ b/src/Pure/Interface/proof_general.ML	Wed Sep 22 21:45:05 1999 +0200
@@ -9,6 +9,7 @@
 sig
   val write_keywords: unit -> unit
   val setup: (theory -> theory) list
+  val thms_containing: xstring list -> unit
   val help: unit -> unit
   val show_context: unit -> theory
   val kill_goal: unit -> unit
@@ -159,6 +160,12 @@
 
 (* some top-level commands for ProofGeneral/isa *)
 
+fun print_thm (a, th) =
+  Pretty.writeln (Pretty.block [Pretty.str (a ^ ":"), Pretty.brk 1,
+    Display.pretty_thm_no_quote (#1 (Drule.freeze_thaw th))]);
+
+val thms_containing = seq print_thm o ThmDatabase.thms_containing;
+
 val help = writeln o Session.welcome;
 val show_context = Context.the_context;