Skip to content
[Jenkins]Jenkins
log in
Success

Changes

Summary

  1. killed dead code
  2. avoid runtime warning with discriminators due to 'Code.del_eqn'
  3. killed deadcode
  4. be more careful before filtering out chained facts in Sledgehammer
Changeset 63314:df655e33995c by blanchet:
killed dead code
The file was modified src/HOL/Tools/BNF/bnf_gfp.ML (diff)
The file was modified src/HOL/Tools/BNF/bnf_gfp_tactics.ML (diff)
Changeset 63313:0c956a9a0ac0 by blanchet:
avoid runtime warning with discriminators due to 'Code.del_eqn'
The file was modified src/HOL/Tools/Ctr_Sugar/ctr_sugar.ML (diff)
Changeset 63312:d75d1e399698 by blanchet:
killed deadcode
The file was modified src/HOL/Tools/BNF/bnf_lfp.ML (diff)
The file was modified src/HOL/Tools/BNF/bnf_lfp_tactics.ML (diff)
Changeset 63311:540cfb14a751 by blanchet:
be more careful before filtering out chained facts in Sledgehammer
The file was modified src/HOL/Tools/Sledgehammer/sledgehammer.ML (diff)