Skip to content
[Jenkins]Jenkins
log in
Success

Changes

Summary

  1. prefer 'xxx' to 'xxx.yyy' to 'xxx(2)' in Sledgehammer, to some extent
  2. tuning
  3. rephrase Nitpick constraint in more first-order format that's also more friendly to the 'box' option
  4. correctly translate constructor argument in 'primrec'
Changeset 73980:291f7b5fc7c9 by blanchet:
prefer 'xxx' to 'xxx.yyy' to 'xxx(2)' in Sledgehammer, to some extent
The file was modified src/HOL/Tools/Sledgehammer/sledgehammer_fact.ML (diff)
Changeset 73979:e5322146e7e8 by blanchet:
tuning
The file was modified src/HOL/TPTP/mash_eval.ML (diff)
The file was modified src/HOL/Tools/Sledgehammer/sledgehammer_fact.ML (diff)
The file was modified src/HOL/Tools/Sledgehammer/sledgehammer_mash.ML (diff)
The file was modified src/HOL/Tools/Sledgehammer/sledgehammer_mepo.ML (diff)
Changeset 73978:906ecb049141 by blanchet:
rephrase Nitpick constraint in more first-order format that's also more friendly to the 'box' option
The file was modified src/HOL/Tools/Nitpick/nitpick_hol.ML (diff)
Changeset 73977:2d8a0f8e30ec by blanchet:
correctly translate constructor argument in 'primrec'
The file was modified src/HOL/Tools/BNF/bnf_lfp_rec_sugar.ML (diff)