equal
deleted
inserted
replaced
102 lemma "True" |
102 lemma "True" |
103 apply(tactic {* sat.sat_tac 1 *}) |
103 apply(tactic {* sat.sat_tac 1 *}) |
104 done |
104 done |
105 |
105 |
106 text {* |
106 text {* |
107 However, for prove anything more exciting you have to use a SAT solver |
107 However, for proving anything more exciting you have to use a SAT solver |
108 that can produce a proof. The internal one is not usuable for this. |
108 that can produce a proof. The internal one is not usuable for this. |
109 |
109 |
110 \begin{readmore} |
110 \begin{readmore} |
111 The interface for the external SAT solvers is implemented |
111 The interface for the external SAT solvers is implemented |
112 in @{ML_file "HOL/Tools/sat_solver.ML"}. This file contains also a simple |
112 in @{ML_file "HOL/Tools/sat_solver.ML"}. This file contains also a simple |