src/Provers/quantifier1.ML
changeset 15027 d23887300b96
parent 13480 bb72bd43c6c3
child 15531 08c8dad8e399
--- a/src/Provers/quantifier1.ML	Thu Jul 08 19:34:18 2004 +0200
+++ b/src/Provers/quantifier1.ML	Thu Jul 08 19:34:56 2004 +0200
@@ -57,10 +57,10 @@
 sig
   val prove_one_point_all_tac: tactic
   val prove_one_point_ex_tac: tactic
-  val rearrange_all: Sign.sg -> thm list -> term -> thm option
-  val rearrange_ex:  Sign.sg -> thm list -> term -> thm option
-  val rearrange_ball: tactic -> Sign.sg -> thm list -> term -> thm option
-  val rearrange_bex:  tactic -> Sign.sg -> thm list -> term -> thm option
+  val rearrange_all: Sign.sg -> simpset -> term -> thm option
+  val rearrange_ex:  Sign.sg -> simpset -> term -> thm option
+  val rearrange_ball: tactic -> Sign.sg -> simpset -> term -> thm option
+  val rearrange_bex:  tactic -> Sign.sg -> simpset -> term -> thm option
 end;
 
 functor Quantifier1Fun(Data: QUANTIFIER1_DATA): QUANTIFIER1 =