equal
deleted
inserted
replaced
1 |
1 |
2 theory Sat |
2 theory Sat |
3 imports "../Appendix" "../FirstSteps" |
3 imports "../Appendix" "../First_Steps" |
4 begin |
4 begin |
5 |
5 |
6 section {* SAT Solvers\label{rec:sat} *} |
6 section {* SAT Solvers\label{rec:sat} *} |
7 |
7 |
8 text {* |
8 text {* |
57 text {* |
57 text {* |
58 returns @{ML "BoolVar 1" in PropLogic} for @{ML pform'} and the table |
58 returns @{ML "BoolVar 1" in PropLogic} for @{ML pform'} and the table |
59 @{ML table'} is: |
59 @{ML table'} is: |
60 |
60 |
61 @{ML_response_fake [display,gray] |
61 @{ML_response_fake [display,gray] |
62 "map (apfst (string_of_term @{context})) (Termtab.dest table')" |
62 "map (apfst (Syntax.string_of_term @{context})) (Termtab.dest table')" |
63 "(\<forall>x. P x, 1)"} |
63 "(\<forall>x. P x, 1)"} |
64 |
64 |
65 In the print out of the tabel, we used some pretty printing scaffolding |
65 In the print out of the tabel, we used some pretty printing scaffolding |
66 to see better which assignment the table contains. |
66 to see better which assignment the table contains. |
67 |
67 |