Skip to content
[Jenkins]Jenkins
log in
Success

Changes

Summary

  1. add reconstruction for the SMT solver veriT * * * Improved veriT reconstruction
  2. NEWS;
  3. activate E 2.5 for production use (see also 5d1a7b688f6d); rebuild component according to current "isabelle build_e" and PLATFORMS;
  4. clarified signature;
  5. clarified Executable.libraries_closure;
  6. dedicated module for toplevel target handling
  7. avoid _cmd suffix where no Isar command is involved
  8. replaced combinators by more conventional nesting pattern
  9. consolidated names and operations
  10. centralized case distinction for beginning and ending nested targets in one place
Changeset 72458:b44e894796d5 by mathias fleury _mathias.fleury@mpi-inf.mpg.de_:
add reconstruction for the SMT solver veriT<br>* * *<br>Improved veriT reconstruction
The file was addedsrc/HOL/SMT_Examples/SMT_Examples_Verit.certs
The file was addedsrc/HOL/SMT_Examples/SMT_Examples_Verit.thy
The file was addedsrc/HOL/SMT_Examples/SMT_Tests_Verit.thy
The file was addedsrc/HOL/Tools/SMT/smt_replay_arith.ML
The file was modified NEWS (diff)
The file was modified src/HOL/ROOT (diff)
The file was modified src/HOL/Real.thy (diff)
The file was modified src/HOL/SMT.thy (diff)
The file was modified src/HOL/Tools/SMT/smt_config.ML (diff)
The file was modified src/HOL/Tools/SMT/smt_replay.ML (diff)
The file was modified src/HOL/Tools/SMT/smt_replay_methods.ML (diff)
The file was modified src/HOL/Tools/SMT/smt_solver.ML (diff)
The file was modified src/HOL/Tools/SMT/smt_systems.ML (diff)
The file was modified src/HOL/Tools/SMT/smtlib_proof.ML (diff)
The file was modified src/HOL/Tools/SMT/verit_isar.ML (diff)
The file was modified src/HOL/Tools/SMT/verit_proof.ML (diff)
The file was modified src/HOL/Tools/SMT/verit_proof_parse.ML (diff)
The file was modified src/HOL/Tools/SMT/verit_replay.ML (diff)
The file was modified src/HOL/Tools/SMT/verit_replay_methods.ML (diff)
The file was modified src/HOL/Tools/SMT/z3_replay_methods.ML (diff)
Changeset 72457:2c7f0ef8323a by wenzelm:
NEWS;
The file was modified NEWS (diff)
Changeset 72456:cd3419427cd3 by wenzelm:
activate E 2.5 for production use (see also 5d1a7b688f6d);<br>rebuild component according to current &quot;isabelle build_e&quot; and PLATFORMS;
The file was modified Admin/components/components.sha1 (diff)
The file was modified Admin/components/main (diff)
Changeset 72455:7bf67a58f54a by wenzelm:
clarified signature;
The file was modified src/Pure/Admin/build_polyml.scala (diff)
The file was modified src/Pure/Admin/build_spass.scala (diff)
The file was modified src/Pure/Admin/build_verit.scala (diff)
The file was modified src/Pure/System/isabelle_system.scala (diff)
Changeset 72454:549391271e74 by wenzelm:
clarified Executable.libraries_closure;
The file was modified src/Pure/System/executable.scala (diff)
Changeset 72453:e4dde7beab39 by haftmann:
dedicated module for toplevel target handling
The file was addedsrc/Pure/Isar/target_context.ML
The file was modified src/Pure/Isar/bundle.ML (diff)
The file was modified src/Pure/Isar/named_target.ML (diff)
The file was modified src/Pure/Isar/toplevel.ML (diff)
The file was modified src/Pure/Pure.thy (diff)
The file was modified src/Pure/ROOT.ML (diff)
Changeset 72452:9017dfa56367 by haftmann:
avoid _cmd suffix where no Isar command is involved
The file was modified src/HOL/Tools/Lifting/lifting_setup.ML (diff)
The file was modified src/Pure/Isar/bundle.ML (diff)
Changeset 72451:e51f1733618d by haftmann:
replaced combinators by more conventional nesting pattern
The file was modified NEWS (diff)
The file was modified src/Pure/Isar/interpretation.ML (diff)
The file was modified src/Pure/Isar/local_theory.ML (diff)
Changeset 72450:24bd1316eaae by haftmann:
consolidated names and operations
The file was modified NEWS (diff)
The file was modified src/HOL/Eisbach/method_closure.ML (diff)
The file was modified src/HOL/Library/code_lazy.ML (diff)
The file was modified src/HOL/Library/datatype_records.ML (diff)
The file was modified src/HOL/Tools/BNF/bnf_def.ML (diff)
The file was modified src/HOL/Tools/BNF/bnf_fp_def_sugar.ML (diff)
The file was modified src/HOL/Tools/BNF/bnf_fp_n2m.ML (diff)
The file was modified src/HOL/Tools/BNF/bnf_fp_util.ML (diff)
The file was modified src/HOL/Tools/BNF/bnf_gfp.ML (diff)
The file was modified src/HOL/Tools/BNF/bnf_gfp_grec.ML (diff)
The file was modified src/HOL/Tools/BNF/bnf_gfp_grec_sugar.ML (diff)
The file was modified src/HOL/Tools/BNF/bnf_lfp.ML (diff)
The file was modified src/HOL/Tools/BNF/bnf_lfp_size.ML (diff)
The file was modified src/HOL/Tools/BNF/bnf_lift.ML (diff)
The file was modified src/HOL/Tools/BNF/bnf_util.ML (diff)
The file was modified src/HOL/Tools/Ctr_Sugar/ctr_sugar.ML (diff)
The file was modified src/HOL/Tools/Lifting/lifting_def.ML (diff)
The file was modified src/HOL/Tools/Lifting/lifting_def_code_dt.ML (diff)
The file was modified src/Pure/Isar/bundle.ML (diff)
The file was modified src/Pure/Isar/local_theory.ML (diff)
The file was modified src/Pure/Isar/toplevel.ML (diff)
Changeset 72449:e1ee4a9902bd by haftmann:
centralized case distinction for beginning and ending nested targets in one place
The file was modified src/Pure/Isar/bundle.ML (diff)
The file was modified src/Pure/Isar/toplevel.ML (diff)