src/HOL/SMT.thy
changeset 57957 e6ee35b8f4b5
parent 57231 dca8d06ecbba
     1.1 --- a/src/HOL/SMT.thy	Sat Aug 16 18:08:55 2014 +0200
     1.2 +++ b/src/HOL/SMT.thy	Sat Aug 16 18:31:47 2014 +0200
     1.3 @@ -126,6 +126,7 @@
     1.4  ML_file "Tools/SMT/z3_proof_tools.ML"
     1.5  ML_file "Tools/SMT/z3_proof_literals.ML"
     1.6  ML_file "Tools/SMT/z3_proof_methods.ML"
     1.7 +named_theorems z3_simp "simplification rules for Z3 proof reconstruction"
     1.8  ML_file "Tools/SMT/z3_proof_reconstruction.ML"
     1.9  ML_file "Tools/SMT/z3_model.ML"
    1.10  ML_file "Tools/SMT/smt_setup_solvers.ML"
    1.11 @@ -135,7 +136,6 @@
    1.12    SMT_Normalize.setup #>
    1.13    SMTLIB_Interface.setup #>
    1.14    Z3_Interface.setup #>
    1.15 -  Z3_Proof_Reconstruction.setup #>
    1.16    SMT_Setup_Solvers.setup
    1.17  *}
    1.18