Summary
- killed dead code
- avoid runtime warning with discriminators due to 'Code.del_eqn'
- killed deadcode
- be more careful before filtering out chained facts in Sledgehammer
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) |
The file was modified | src/HOL/Tools/Ctr_Sugar/ctr_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_tactics.ML (diff) |
The file was modified | src/HOL/Tools/Sledgehammer/sledgehammer.ML (diff) |