# HG changeset patch
# User webertj
# Date 1129133868 -7200
# Node ID 0a451f041853de3e225b8f1b8aea382a25ecc880
# Parent  e661a78472f0ee3563a0e612d308a763648e3760
counter added to SAT signature

diff -r e661a78472f0 -r 0a451f041853 src/HOL/Tools/sat_funcs.ML
--- 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 =