src/HOL/SMT.thy
changeset 58360 dee1fd1cc631
parent 58072 a86c962de77f
child 58441 c1b489999de9
     1.1 --- a/src/HOL/SMT.thy	Wed Sep 17 16:20:13 2014 +0200
     1.2 +++ b/src/HOL/SMT.thy	Wed Sep 17 16:53:39 2014 +0200
     1.3 @@ -112,15 +112,16 @@
     1.4  ML_file "Tools/SMT/z3_proof.ML"
     1.5  ML_file "Tools/SMT/z3_isar.ML"
     1.6  ML_file "Tools/SMT/smt_solver.ML"
     1.7 +ML_file "Tools/SMT/cvc4_interface.ML"
     1.8 +ML_file "Tools/SMT/verit_proof.ML"
     1.9 +ML_file "Tools/SMT/verit_isar.ML"
    1.10 +ML_file "Tools/SMT/verit_proof_parse.ML"
    1.11  ML_file "Tools/SMT/z3_interface.ML"
    1.12  ML_file "Tools/SMT/z3_replay_util.ML"
    1.13  ML_file "Tools/SMT/z3_replay_literals.ML"
    1.14  ML_file "Tools/SMT/z3_replay_rules.ML"
    1.15  ML_file "Tools/SMT/z3_replay_methods.ML"
    1.16  ML_file "Tools/SMT/z3_replay.ML"
    1.17 -ML_file "Tools/SMT/verit_proof.ML"
    1.18 -ML_file "Tools/SMT/verit_isar.ML"
    1.19 -ML_file "Tools/SMT/verit_proof_parse.ML"
    1.20  ML_file "Tools/SMT/smt_systems.ML"
    1.21  
    1.22  method_setup smt = {*
    1.23 @@ -196,6 +197,14 @@
    1.24  declare [[smt_infer_triggers = false]]
    1.25  
    1.26  text {*
    1.27 +Enable the following option to use built-in support for datatypes,
    1.28 +codatatypes, and records in CVC4. Currently, this is implemented only
    1.29 +in oracle mode.
    1.30 +*}
    1.31 +
    1.32 +declare [[cvc4_extensions = false]]
    1.33 +
    1.34 +text {*
    1.35  Enable the following option to use built-in support for div/mod, datatypes,
    1.36  and records in Z3. Currently, this is implemented only in oracle mode.
    1.37  *}