src/Provers/classical.ML
changeset 50062 e038198f7d08
parent 48126 cdbdbfa6a29f
child 50108 f171b5240c31
     1.1 --- a/src/Provers/classical.ML	Wed Nov 14 14:45:14 2012 +0100
     1.2 +++ b/src/Provers/classical.ML	Sat Nov 03 19:07:07 2012 +0100
     1.3 @@ -24,8 +24,9 @@
     1.4    val not_elim: thm  (* ~P ==> P ==> R *)
     1.5    val swap: thm  (* ~ P ==> (~ R ==> P) ==> R *)
     1.6    val classical: thm  (* (~ P ==> P) ==> P *)
     1.7 -  val sizef: thm -> int  (* size function for BEST_FIRST *)
     1.8 -  val hyp_subst_tacs: (int -> tactic) list
     1.9 +  val sizef: thm -> int  (* size function for BEST_FIRST, typically size_of_thm *)
    1.10 +  val hyp_subst_tacs: (int -> tactic) list (* optional tactics for substitution in
    1.11 +    the hypotheses; assumed to be safe! *)
    1.12  end;
    1.13  
    1.14  signature BASIC_CLASSICAL =