src/Pure/Interface/proof_general.ML
changeset 7579 20adf381fb0a
parent 7407 fc8cad55af74
child 7581 18070ae7a84c
     1.1 --- a/src/Pure/Interface/proof_general.ML	Wed Sep 22 21:04:55 1999 +0200
     1.2 +++ b/src/Pure/Interface/proof_general.ML	Wed Sep 22 21:45:05 1999 +0200
     1.3 @@ -9,6 +9,7 @@
     1.4  sig
     1.5    val write_keywords: unit -> unit
     1.6    val setup: (theory -> theory) list
     1.7 +  val thms_containing: xstring list -> unit
     1.8    val help: unit -> unit
     1.9    val show_context: unit -> theory
    1.10    val kill_goal: unit -> unit
    1.11 @@ -159,6 +160,12 @@
    1.12  
    1.13  (* some top-level commands for ProofGeneral/isa *)
    1.14  
    1.15 +fun print_thm (a, th) =
    1.16 +  Pretty.writeln (Pretty.block [Pretty.str (a ^ ":"), Pretty.brk 1,
    1.17 +    Display.pretty_thm_no_quote (#1 (Drule.freeze_thaw th))]);
    1.18 +
    1.19 +val thms_containing = seq print_thm o ThmDatabase.thms_containing;
    1.20 +
    1.21  val help = writeln o Session.welcome;
    1.22  val show_context = Context.the_context;
    1.23