equal
deleted
inserted
replaced
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 Record |
|
9 keywords "smt_status" :: diag |
9 uses |
10 uses |
10 "Tools/SMT/smt_utils.ML" |
11 "Tools/SMT/smt_utils.ML" |
11 "Tools/SMT/smt_failure.ML" |
12 "Tools/SMT/smt_failure.ML" |
12 "Tools/SMT/smt_config.ML" |
13 "Tools/SMT/smt_config.ML" |
13 ("Tools/SMT/smt_builtin.ML") |
14 ("Tools/SMT/smt_builtin.ML") |