src/Pure/display.ML
changeset 26928 ca87aff1ad2d
parent 26637 0bfccafc52eb
child 26939 1035c89b4c02
     1.1 --- a/src/Pure/display.ML	Fri May 16 23:25:37 2008 +0200
     1.2 +++ b/src/Pure/display.ML	Sat May 17 13:54:30 2008 +0200
     1.3 @@ -11,17 +11,6 @@
     1.4    val goals_limit: int ref
     1.5    val show_hyps: bool ref
     1.6    val show_tags: bool ref
     1.7 -  val string_of_thm: thm -> string
     1.8 -  val print_thm: thm -> unit
     1.9 -  val print_thms: thm list -> unit
    1.10 -  val prth: thm -> thm
    1.11 -  val prthq: thm Seq.seq -> thm Seq.seq
    1.12 -  val prths: thm list -> thm list
    1.13 -  val string_of_ctyp: ctyp -> string
    1.14 -  val print_ctyp: ctyp -> unit
    1.15 -  val string_of_cterm: cterm -> string
    1.16 -  val print_cterm: cterm -> unit
    1.17 -  val print_syntax: theory -> unit
    1.18    val show_consts: bool ref
    1.19  end;
    1.20  
    1.21 @@ -31,11 +20,22 @@
    1.22    val pretty_flexpair: Pretty.pp -> term * term -> Pretty.T
    1.23    val pretty_thm_aux: Pretty.pp -> bool -> bool -> term list -> thm -> Pretty.T
    1.24    val pretty_thm: thm -> Pretty.T
    1.25 +  val string_of_thm: thm -> string
    1.26    val pretty_thms: thm list -> Pretty.T
    1.27    val pretty_thm_sg: theory -> thm -> Pretty.T
    1.28    val pretty_thms_sg: theory -> thm list -> Pretty.T
    1.29 +  val print_thm: thm -> unit
    1.30 +  val print_thms: thm list -> unit
    1.31 +  val prth: thm -> thm
    1.32 +  val prthq: thm Seq.seq -> thm Seq.seq
    1.33 +  val prths: thm list -> thm list
    1.34    val pretty_ctyp: ctyp -> Pretty.T
    1.35 +  val string_of_ctyp: ctyp -> string
    1.36 +  val print_ctyp: ctyp -> unit
    1.37    val pretty_cterm: cterm -> Pretty.T
    1.38 +  val string_of_cterm: cterm -> string
    1.39 +  val print_cterm: cterm -> unit
    1.40 +  val print_syntax: theory -> unit
    1.41    val pretty_full_theory: bool -> theory -> Pretty.T list
    1.42    val pretty_goals_aux: Pretty.pp -> Markup.T -> bool * bool -> int -> thm -> Pretty.T list
    1.43    val pretty_goals: int -> thm -> Pretty.T list