src/HOL/SMT.thy
changeset 59015 627a93f67182
parent 58889 5b7a9633cfa8
child 59017 80290f06a810
     1.1 --- a/src/HOL/SMT.thy	Wed Nov 19 10:31:15 2014 +0100
     1.2 +++ b/src/HOL/SMT.thy	Wed Nov 19 10:31:15 2014 +0100
     1.3 @@ -159,6 +159,7 @@
     1.4  ML_file "Tools/SMT/z3_isar.ML"
     1.5  ML_file "Tools/SMT/smt_solver.ML"
     1.6  ML_file "Tools/SMT/cvc4_interface.ML"
     1.7 +ML_file "Tools/SMT/cvc4_proof_parse.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"