changeset 57226 | c22ad39c3b4b |
parent 57213 | 9daec42f6784 |
child 57229 | 489083abce44 |
57225:ff69e42ccf92 | 57226:c22ad39c3b4b |
---|---|
3 *) |
3 *) |
4 |
4 |
5 header {* Bindings to Satisfiability Modulo Theories (SMT) solvers *} |
5 header {* Bindings to Satisfiability Modulo Theories (SMT) solvers *} |
6 |
6 |
7 theory SMT |
7 theory SMT |
8 imports Record |
8 imports List |
9 keywords "smt_status" :: diag |
9 keywords "smt_status" :: diag |
10 begin |
10 begin |
11 |
11 |
12 ML_file "Tools/SMT/smt_utils.ML" |
12 ML_file "Tools/SMT/smt_utils.ML" |
13 ML_file "Tools/SMT/smt_failure.ML" |
13 ML_file "Tools/SMT/smt_failure.ML" |