src/HOL/Library/Old_SMT.thy
changeset 58058 1a0b18176548
parent 58057 883f3c4c928e
child 58059 4e477dcd050a
     1.1 --- a/src/HOL/Library/Old_SMT.thy	Thu Aug 28 00:40:38 2014 +0200
     1.2 +++ b/src/HOL/Library/Old_SMT.thy	Thu Aug 28 00:40:38 2014 +0200
     1.3 @@ -9,9 +9,9 @@
     1.4  keywords "smt_status" :: diag
     1.5  begin
     1.6  
     1.7 -ML_file "Old_SMT/smt_utils.ML"
     1.8 -ML_file "Old_SMT/smt_failure.ML"
     1.9 -ML_file "Old_SMT/smt_config.ML"
    1.10 +ML_file "Old_SMT/old_smt_utils.ML"
    1.11 +ML_file "Old_SMT/old_smt_failure.ML"
    1.12 +ML_file "Old_SMT/old_smt_config.ML"
    1.13  
    1.14  
    1.15  subsection {* Triggers for quantifier instantiation *}
    1.16 @@ -115,34 +115,34 @@
    1.17  
    1.18  subsection {* Setup *}
    1.19  
    1.20 -ML_file "Old_SMT/smt_builtin.ML"
    1.21 -ML_file "Old_SMT/smt_datatypes.ML"
    1.22 -ML_file "Old_SMT/smt_normalize.ML"
    1.23 -ML_file "Old_SMT/smt_translate.ML"
    1.24 -ML_file "Old_SMT/smt_solver.ML"
    1.25 -ML_file "Old_SMT/smtlib_interface.ML"
    1.26 -ML_file "Old_SMT/z3_interface.ML"
    1.27 -ML_file "Old_SMT/z3_proof_parser.ML"
    1.28 -ML_file "Old_SMT/z3_proof_tools.ML"
    1.29 -ML_file "Old_SMT/z3_proof_literals.ML"
    1.30 -ML_file "Old_SMT/z3_proof_methods.ML"
    1.31 +ML_file "Old_SMT/old_smt_builtin.ML"
    1.32 +ML_file "Old_SMT/old_smt_datatypes.ML"
    1.33 +ML_file "Old_SMT/old_smt_normalize.ML"
    1.34 +ML_file "Old_SMT/old_smt_translate.ML"
    1.35 +ML_file "Old_SMT/old_smt_solver.ML"
    1.36 +ML_file "Old_SMT/old_smtlib_interface.ML"
    1.37 +ML_file "Old_SMT/old_z3_interface.ML"
    1.38 +ML_file "Old_SMT/old_z3_proof_parser.ML"
    1.39 +ML_file "Old_SMT/old_z3_proof_tools.ML"
    1.40 +ML_file "Old_SMT/old_z3_proof_literals.ML"
    1.41 +ML_file "Old_SMT/old_z3_proof_methods.ML"
    1.42  named_theorems z3_simp "simplification rules for Z3 proof reconstruction"
    1.43 -ML_file "Old_SMT/z3_proof_reconstruction.ML"
    1.44 -ML_file "Old_SMT/z3_model.ML"
    1.45 -ML_file "Old_SMT/smt_setup_solvers.ML"
    1.46 +ML_file "Old_SMT/old_z3_proof_reconstruction.ML"
    1.47 +ML_file "Old_SMT/old_z3_model.ML"
    1.48 +ML_file "Old_SMT/old_smt_setup_solvers.ML"
    1.49  
    1.50  setup {*
    1.51 -  SMT_Config.setup #>
    1.52 -  SMT_Normalize.setup #>
    1.53 -  SMTLIB_Interface.setup #>
    1.54 -  Z3_Interface.setup #>
    1.55 -  SMT_Setup_Solvers.setup
    1.56 +  Old_SMT_Config.setup #>
    1.57 +  Old_SMT_Normalize.setup #>
    1.58 +  Old_SMTLIB_Interface.setup #>
    1.59 +  Old_Z3_Interface.setup #>
    1.60 +  Old_SMT_Setup_Solvers.setup
    1.61  *}
    1.62  
    1.63  method_setup smt = {*
    1.64    Scan.optional Attrib.thms [] >>
    1.65      (fn thms => fn ctxt =>
    1.66 -      METHOD (fn facts => HEADGOAL (SMT_Solver.smt_tac ctxt (thms @ facts))))
    1.67 +      METHOD (fn facts => HEADGOAL (Old_SMT_Solver.smt_tac ctxt (thms @ facts))))
    1.68  *} "apply an SMT solver to the current goal"
    1.69  
    1.70  
    1.71 @@ -419,11 +419,11 @@
    1.72    "(if P then Q else \<not>R) \<or> P \<or> R"
    1.73    by auto
    1.74  
    1.75 -ML_file "Old_SMT/smt_real.ML"
    1.76 -setup SMT_Real.setup
    1.77 +ML_file "Old_SMT/old_smt_real.ML"
    1.78 +setup Old_SMT_Real.setup
    1.79  
    1.80 -ML_file "Old_SMT/smt_word.ML"
    1.81 -setup SMT_Word.setup
    1.82 +ML_file "Old_SMT/old_smt_word.ML"
    1.83 +setup Old_SMT_Word.setup
    1.84  
    1.85  hide_type (open) pattern
    1.86  hide_const fun_app term_true term_false z3div z3mod