Skip to content
[Jenkins]Jenkins
log in
Success

Changes

Summary

  1. avoid code generator warnings when deleting equations in BNF commands (e.g., datatype) in locales with assumptions and similar
  2. adapted Nunchaku integration to keyword renaming
Changeset 64430:1d85ac286c72 by blanchet:
avoid code generator warnings when deleting equations in BNF commands (e.g., datatype) in locales with assumptions and similar
The file was modified src/HOL/Ctr_Sugar.thy (diff)
The file was modified src/HOL/Tools/Ctr_Sugar/ctr_sugar.ML (diff)
The file was modified src/HOL/Tools/Ctr_Sugar/ctr_sugar_tactics.ML (diff)
The file was modified src/HOL/Tools/Quickcheck/quickcheck_common.ML (diff)
The file was modified src/Pure/Isar/code.ML (diff)
Changeset 64429:582f54f6b29b by blanchet:
adapted Nunchaku integration to keyword renaming
The file was modified src/HOL/Nunchaku/Tools/nunchaku_problem.ML (diff)
The file was modified src/HOL/Tools/Sledgehammer/sledgehammer_isar_annotate.ML (diff)