src/HOL/SMT.thy
changeset 57226 c22ad39c3b4b
parent 57213 9daec42f6784
child 57229 489083abce44
equal deleted inserted replaced
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"