| changeset 17843 | 0a451f041853 |
| parent 17842 | e661a78472f0 |
| child 19236 | 150e8b0fb991 |
--- a/src/HOL/Tools/sat_funcs.ML Wed Oct 12 17:06:22 2005 +0200 +++ b/src/HOL/Tools/sat_funcs.ML Wed Oct 12 18:17:48 2005 +0200 @@ -55,6 +55,7 @@ val trace_sat : bool ref (* print trace messages *) val sat_tac : int -> Tactical.tactic val satx_tac : int -> Tactical.tactic + val counter : int ref (* number of resolution steps during last proof replay *) end functor SATFunc (structure cnf : CNF) : SAT =