Skip to content
[Jenkins]Jenkins
log in
Success

Changes

Summary

  1. updated NEWS
  2. optimized parent computation in MaSh
  3. avoid loading MaSh file first time around for higher responsiveness of Sledgehammer
  4. tuned MaSh's metacharacters to avoid needless decoding
  5. optimization in MaSh parsing
  6. tuned ML
  7. removed trailing final stops in Nitpick messages
  8. killed final stops in Sledgehammer and friends
  9. tuned message
  10. tuning punctuation in messages output by Isabelle
  11. tuning whitespace in output syntax
Changeset 63699:6910c5ce74d3 by blanchet:
updated NEWS
The file was modified NEWS (diff)
Changeset 63698:4de35d16e533 by blanchet:
optimized parent computation in MaSh
The file was modified src/HOL/Tools/Sledgehammer/sledgehammer_mash.ML (diff)
Changeset 63697:0afe49623cf9 by blanchet:
avoid loading MaSh file first time around for higher responsiveness of Sledgehammer
The file was modified src/HOL/Tools/Sledgehammer/sledgehammer.ML (diff)
The file was modified src/HOL/Tools/Sledgehammer/sledgehammer_mash.ML (diff)
Changeset 63696:af310e622d64 by blanchet:
tuned MaSh's metacharacters to avoid needless decoding
The file was modified src/HOL/Tools/Sledgehammer/sledgehammer_mash.ML (diff)
Changeset 63695:9ad6a63cc8bd by blanchet:
optimization in MaSh parsing
The file was modified src/HOL/Tools/Sledgehammer/sledgehammer.ML (diff)
The file was modified src/HOL/Tools/Sledgehammer/sledgehammer_mash.ML (diff)
Changeset 63694:e58bcea9492a by blanchet:
tuned ML
The file was modified src/HOL/Tools/ATP/atp_problem_generate.ML (diff)
The file was modified src/HOL/Tools/BNF/bnf_fp_def_sugar.ML (diff)
The file was modified src/HOL/Tools/Sledgehammer/sledgehammer.ML (diff)
Changeset 63693:5b02f7757a4c by blanchet:
removed trailing final stops in Nitpick messages
The file was modified src/HOL/Tools/Nitpick/kodkod_sat.ML (diff)
The file was modified src/HOL/Tools/Nitpick/nitpick.ML (diff)
The file was modified src/HOL/Tools/Nitpick/nitpick_commands.ML (diff)
The file was modified src/HOL/Tools/Nitpick/nitpick_hol.ML (diff)
The file was modified src/HOL/Tools/Nitpick/nitpick_tests.ML (diff)
Changeset 63692:1bc4bc2c9fd1 by blanchet:
killed final stops in Sledgehammer and friends
The file was modified src/HOL/Mirabelle/Tools/mirabelle_sledgehammer.ML (diff)
The file was modified src/HOL/TPTP/mash_eval.ML (diff)
The file was modified src/HOL/TPTP/mash_export.ML (diff)
The file was modified src/HOL/Tools/ATP/atp_problem_generate.ML (diff)
The file was modified src/HOL/Tools/ATP/atp_proof.ML (diff)
The file was modified src/HOL/Tools/ATP/atp_proof_reconstruct.ML (diff)
The file was modified src/HOL/Tools/ATP/atp_satallax.ML (diff)
The file was modified src/HOL/Tools/ATP/atp_systems.ML (diff)
The file was modified src/HOL/Tools/Sledgehammer/async_manager_legacy.ML (diff)
The file was modified src/HOL/Tools/Sledgehammer/sledgehammer.ML (diff)
The file was modified src/HOL/Tools/Sledgehammer/sledgehammer_commands.ML (diff)
The file was modified src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML (diff)
The file was modified src/HOL/Tools/Sledgehammer/sledgehammer_mash.ML (diff)
The file was modified src/HOL/Tools/Sledgehammer/sledgehammer_proof_methods.ML (diff)
The file was modified src/HOL/Tools/Sledgehammer/sledgehammer_prover.ML (diff)
The file was modified src/HOL/Tools/Sledgehammer/sledgehammer_prover_atp.ML (diff)
The file was modified src/HOL/Tools/Sledgehammer/sledgehammer_prover_minimize.ML (diff)
The file was modified src/HOL/Tools/Sledgehammer/sledgehammer_prover_smt.ML (diff)
The file was modified src/HOL/Tools/Sledgehammer/sledgehammer_util.ML (diff)
Changeset 63691:94a89b95b871 by blanchet:
tuned message
The file was modified src/HOL/Tools/BNF/bnf_gfp_grec.ML (diff)
Changeset 63690:48a2c88091d7 by blanchet:
tuning punctuation in messages output by Isabelle
The file was modified src/HOL/Tools/try0.ML (diff)
The file was modified src/Tools/try.ML (diff)
Changeset 63689:61171cbeedde by blanchet:
tuning whitespace in output syntax
The file was modified src/HOL/Library/Multiset.thy (diff)