Skip to content
[Jenkins]Jenkins
log in
Success

Changes

Summary

  1. strengthened tactics
  2. derive relator properties forward
  3. derive maps forward
  4. tuning
  5. tuning
  6. provide a mechanism for ensuring dead type variables occur in typedef if desired
  7. preserve order of dead variables
  8. tuning
Changeset 63842:f738df816abf by blanchet:
strengthened tactics
The file was modified src/HOL/Tools/BNF/bnf_fp_def_sugar.ML (diff)
The file was modified src/HOL/Tools/BNF/bnf_fp_def_sugar_tactics.ML (diff)
Changeset 63841:813a574da746 by blanchet:
derive relator properties forward
The file was modified src/HOL/Tools/BNF/bnf_fp_def_sugar.ML (diff)
The file was modified src/HOL/Tools/BNF/bnf_fp_def_sugar_tactics.ML (diff)
Changeset 63840:eb6d2aace13a by blanchet:
derive maps forward
The file was modified src/HOL/Tools/BNF/bnf_fp_def_sugar.ML (diff)
The file was modified src/HOL/Tools/BNF/bnf_fp_def_sugar_tactics.ML (diff)
Changeset 63839:fe7841fa2a9b by blanchet:
tuning
The file was modified src/HOL/Tools/BNF/bnf_fp_def_sugar.ML (diff)
Changeset 63838:6f74e9aea816 by blanchet:
tuning
The file was modified src/HOL/Tools/BNF/bnf_fp_def_sugar.ML (diff)
Changeset 63837:fdf90aa59868 by blanchet:
provide a mechanism for ensuring dead type variables occur in typedef if desired
The file was modified src/HOL/Tools/BNF/bnf_comp.ML (diff)
The file was modified src/HOL/Tools/BNF/bnf_fp_util.ML (diff)
Changeset 63836:2f9ee7d85d85 by blanchet:
preserve order of dead variables
The file was modified src/HOL/Tools/BNF/bnf_comp.ML (diff)
Changeset 63835:4f8c6e63bc41 by blanchet:
tuning
The file was modified src/HOL/Tools/BNF/bnf_fp_def_sugar_tactics.ML (diff)