src/Provers/quantifier1.ML
changeset 15027 d23887300b96
parent 13480 bb72bd43c6c3
child 15531 08c8dad8e399
     1.1 --- a/src/Provers/quantifier1.ML	Thu Jul 08 19:34:18 2004 +0200
     1.2 +++ b/src/Provers/quantifier1.ML	Thu Jul 08 19:34:56 2004 +0200
     1.3 @@ -57,10 +57,10 @@
     1.4  sig
     1.5    val prove_one_point_all_tac: tactic
     1.6    val prove_one_point_ex_tac: tactic
     1.7 -  val rearrange_all: Sign.sg -> thm list -> term -> thm option
     1.8 -  val rearrange_ex:  Sign.sg -> thm list -> term -> thm option
     1.9 -  val rearrange_ball: tactic -> Sign.sg -> thm list -> term -> thm option
    1.10 -  val rearrange_bex:  tactic -> Sign.sg -> thm list -> term -> thm option
    1.11 +  val rearrange_all: Sign.sg -> simpset -> term -> thm option
    1.12 +  val rearrange_ex:  Sign.sg -> simpset -> term -> thm option
    1.13 +  val rearrange_ball: tactic -> Sign.sg -> simpset -> term -> thm option
    1.14 +  val rearrange_bex:  tactic -> Sign.sg -> simpset -> term -> thm option
    1.15  end;
    1.16  
    1.17  functor Quantifier1Fun(Data: QUANTIFIER1_DATA): QUANTIFIER1 =