src/Pure/drule.ML
changeset 67 8380bc0adde7
parent 11 d0e17c42dbb4
child 199 ac55692ab41f
equal deleted inserted replaced
66:1b14cd923772 67:8380bc0adde7
    34   val MRL: thm list list * thm list -> thm list
    34   val MRL: thm list list * thm list -> thm list
    35   val MRS: thm list * thm -> thm
    35   val MRS: thm list * thm -> thm
    36   val print_cterm: Sign.cterm -> unit
    36   val print_cterm: Sign.cterm -> unit
    37   val print_ctyp: Sign.ctyp -> unit
    37   val print_ctyp: Sign.ctyp -> unit
    38   val print_goals: int -> thm -> unit
    38   val print_goals: int -> thm -> unit
       
    39   val print_goals_ref: (int -> thm -> unit) ref
    39   val print_sg: Sign.sg -> unit
    40   val print_sg: Sign.sg -> unit
    40   val print_theory: theory -> unit
    41   val print_theory: theory -> unit
    41   val pprint_sg: Sign.sg -> pprint_args -> unit
    42   val pprint_sg: Sign.sg -> pprint_args -> unit
    42   val pprint_theory: theory -> pprint_args -> unit
    43   val pprint_theory: theory -> pprint_args -> unit
    43   val print_thm: thm -> unit
    44   val print_thm: thm -> unit
   330 	      writeln("A total of " ^ string_of_int ngoals ^ " subgoals..."))
   331 	      writeln("A total of " ^ string_of_int ngoals ^ " subgoals..."))
   331         else printgoals (1, As);
   332         else printgoals (1, As);
   332    printff tpairs
   333    printff tpairs
   333 end;
   334 end;
   334 
   335 
       
   336 (*"hook" for user interfaces: allows print_goals to be replaced*)
       
   337 val print_goals_ref = ref print_goals;
   335 
   338 
   336 (** theorem equality test is exported and used by BEST_FIRST **)
   339 (** theorem equality test is exported and used by BEST_FIRST **)
   337 
   340 
   338 (*equality of signatures means exact identity -- by ref equality*)
   341 (*equality of signatures means exact identity -- by ref equality*)
   339 fun eq_sg (sg1,sg2) = (#stamps(Sign.rep_sg sg1) = #stamps(Sign.rep_sg sg2));
   342 fun eq_sg (sg1,sg2) = (#stamps(Sign.rep_sg sg1) = #stamps(Sign.rep_sg sg2));