# HG changeset patch # User wenzelm # Date 1255789994 -7200 # Node ID 1df87354c3081665ea92a93751d146e3d3b0c177 # Parent 5b21661fe618353ba340a09dc580528816606410 Unsynchronized.set etc.; diff -r 5b21661fe618 -r 1df87354c308 src/HOL/ex/SAT_Examples.thy --- a/src/HOL/ex/SAT_Examples.thy Sat Oct 17 15:57:51 2009 +0200 +++ b/src/HOL/ex/SAT_Examples.thy Sat Oct 17 16:33:14 2009 +0200 @@ -7,13 +7,12 @@ header {* Examples for the 'sat' and 'satx' tactic *} theory SAT_Examples imports Main - begin (* ML {* sat.solver := "zchaff_with_proofs"; *} *) (* ML {* sat.solver := "minisat_with_proofs"; *} *) -ML {* set sat.trace_sat; *} -ML {* set quick_and_dirty; *} +ML {* Unsynchronized.set sat.trace_sat; *} +ML {* Unsynchronized.set quick_and_dirty; *} lemma "True" by sat @@ -79,8 +78,8 @@ lemma "(ALL x. P x) | ~ All P" by sat -ML {* reset sat.trace_sat; *} -ML {* reset quick_and_dirty; *} +ML {* Unsynchronized.reset sat.trace_sat; *} +ML {* Unsynchronized.reset quick_and_dirty; *} method_setup rawsat = {* Scan.succeed (SIMPLE_METHOD' o sat.rawsat_tac) *}