equal
deleted
inserted
replaced
99 There are also two tactics that make use of SAT solvers. One |
99 There are also two tactics that make use of SAT solvers. One |
100 is the tactic @{ML sat_tac in sat}. For example |
100 is the tactic @{ML sat_tac in sat}. For example |
101 *} |
101 *} |
102 |
102 |
103 lemma "True" |
103 lemma "True" |
104 apply(tactic {* sat.sat_tac 1 *}) |
104 apply(tactic {* sat.sat_tac @{context} 1 *}) |
105 done |
105 done |
106 |
106 |
107 text {* |
107 text {* |
108 However, for proving anything more exciting using @{ML "sat_tac" in sat} you |
108 However, for proving anything more exciting using @{ML "sat_tac" in sat} you |
109 have to use a SAT solver that can produce a proof. The internal |
109 have to use a SAT solver that can produce a proof. The internal |