--- a/src/Tools/Metis/src/Active.sig Mon Sep 13 16:44:20 2010 +0200
+++ b/src/Tools/Metis/src/Active.sig Mon Sep 13 21:24:10 2010 +0200
@@ -1,6 +1,6 @@
(* ========================================================================= *)
(* THE ACTIVE SET OF CLAUSES *)
-(* Copyright (c) 2002-2006 Joe Hurd, distributed under the BSD License *)
+(* Copyright (c) 2002-2006 Joe Hurd, distributed under the BSD License *)
(* ========================================================================= *)
signature Active =
@@ -10,7 +10,10 @@
(* A type of active clause sets. *)
(* ------------------------------------------------------------------------- *)
-type simplify = {subsume : bool, reduce : bool, rewrite : bool}
+type simplify =
+ {subsume : bool,
+ reduce : bool,
+ rewrite : bool}
type parameters =
{clause : Clause.parameters,
@@ -27,13 +30,15 @@
val size : active -> int
-val saturated : active -> Clause.clause list
+val saturation : active -> Clause.clause list
(* ------------------------------------------------------------------------- *)
(* Create a new active clause set and initialize clauses. *)
(* ------------------------------------------------------------------------- *)
-val new : parameters -> Thm.thm list -> active * Clause.clause list
+val new :
+ parameters -> {axioms : Thm.thm list, conjecture : Thm.thm list} ->
+ active * {axioms : Clause.clause list, conjecture : Clause.clause list}
(* ------------------------------------------------------------------------- *)
(* Add a clause into the active set and deduce all consequences. *)
@@ -45,6 +50,6 @@
(* Pretty printing. *)
(* ------------------------------------------------------------------------- *)
-val pp : active Parser.pp
+val pp : active Print.pp
end