pretty_thm is now exported;
authorwenzelm
Tue Dec 21 14:47:29 1993 +0100 (1993-12-21)
changeset 199ac55692ab41f
parent 198 0f0ff91b07f6
child 200 39a931cc6558
pretty_thm is now exported;
src/Pure/drule.ML
     1.1 --- a/src/Pure/drule.ML	Tue Dec 21 13:58:12 1993 +0100
     1.2 +++ b/src/Pure/drule.ML	Tue Dec 21 14:47:29 1993 +0100
     1.3 @@ -1,4 +1,4 @@
     1.4 -(*  Title: 	drule
     1.5 +(*  Title: 	Pure/drule.ML
     1.6      ID:         $Id$
     1.7      Author: 	Lawrence C Paulson, Cambridge University Computer Laboratory
     1.8      Copyright   1993  University of Cambridge
     1.9 @@ -41,6 +41,7 @@
    1.10    val print_theory: theory -> unit
    1.11    val pprint_sg: Sign.sg -> pprint_args -> unit
    1.12    val pprint_theory: theory -> pprint_args -> unit
    1.13 +  val pretty_thm: thm -> Sign.Syntax.Pretty.T
    1.14    val print_thm: thm -> unit
    1.15    val prth: thm -> thm
    1.16    val prthq: thm Sequence.seq -> thm Sequence.seq