src/Pure/drule.ML
changeset 199 ac55692ab41f
parent 67 8380bc0adde7
child 210 49497bdf573e
equal deleted inserted replaced
198:0f0ff91b07f6 199:ac55692ab41f
     1 (*  Title: 	drule
     1 (*  Title: 	Pure/drule.ML
     2     ID:         $Id$
     2     ID:         $Id$
     3     Author: 	Lawrence C Paulson, Cambridge University Computer Laboratory
     3     Author: 	Lawrence C Paulson, Cambridge University Computer Laboratory
     4     Copyright   1993  University of Cambridge
     4     Copyright   1993  University of Cambridge
     5 
     5 
     6 Derived rules and other operations on theorems and theories
     6 Derived rules and other operations on theorems and theories
    39   val print_goals_ref: (int -> thm -> unit) ref
    39   val print_goals_ref: (int -> thm -> unit) ref
    40   val print_sg: Sign.sg -> unit
    40   val print_sg: Sign.sg -> unit
    41   val print_theory: theory -> unit
    41   val print_theory: theory -> unit
    42   val pprint_sg: Sign.sg -> pprint_args -> unit
    42   val pprint_sg: Sign.sg -> pprint_args -> unit
    43   val pprint_theory: theory -> pprint_args -> unit
    43   val pprint_theory: theory -> pprint_args -> unit
       
    44   val pretty_thm: thm -> Sign.Syntax.Pretty.T
    44   val print_thm: thm -> unit
    45   val print_thm: thm -> unit
    45   val prth: thm -> thm
    46   val prth: thm -> thm
    46   val prthq: thm Sequence.seq -> thm Sequence.seq
    47   val prthq: thm Sequence.seq -> thm Sequence.seq
    47   val prths: thm list -> thm list
    48   val prths: thm list -> thm list
    48   val read_instantiate: (string*string)list -> thm -> thm
    49   val read_instantiate: (string*string)list -> thm -> thm