Summary
- avoid code generator warnings when deleting equations in BNF commands (e.g., datatype) in locales with assumptions and similar
- adapted Nunchaku integration to keyword renaming
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) |
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) |