export prems_of;
authorwenzelm
Tue Sep 21 17:24:50 1999 +0200 (1999-09-21)
changeset 75571b977741f530
parent 7556 f3e78ebcf6ba
child 7558 08b2d5c94b8a
export prems_of;
src/Pure/Isar/proof_context.ML
     1.1 --- a/src/Pure/Isar/proof_context.ML	Tue Sep 21 17:24:35 1999 +0200
     1.2 +++ b/src/Pure/Isar/proof_context.ML	Tue Sep 21 17:24:50 1999 +0200
     1.3 @@ -11,6 +11,7 @@
     1.4    exception CONTEXT of string * context
     1.5    val theory_of: context -> theory
     1.6    val sign_of: context -> Sign.sg
     1.7 +  val prems_of: context -> thm list
     1.8    val show_hyps: bool ref
     1.9    val pretty_thm: thm -> Pretty.T
    1.10    val verbose: bool ref