Skip to content
Success

Changes

Summary

  1. NEWS
  2. strengthened tactic
  3. avoid warning triggered by code generator
  4. strengthened tactic
  5. prove 'set' property backward
Changeset 63855:40f34614bd06 by blanchet:
NEWS
The file was modified NEWS (diff)
Changeset 63854:e90f51b20215 by blanchet:
strengthened tactic
The file was modified src/HOL/Tools/BNF/bnf_fp_def_sugar_tactics.ML (diff)
Changeset 63853:d0e8921da311 by blanchet:
avoid warning triggered by code generator
The file was modified src/HOL/Tools/BNF/bnf_fp_def_sugar.ML (diff)
The file was modified src/HOL/Tools/Ctr_Sugar/ctr_sugar.ML (diff)
Changeset 63852:0a6b145879f4 by blanchet:
strengthened tactic
The file was modified src/HOL/Tools/BNF/bnf_fp_def_sugar_tactics.ML (diff)
Changeset 63851:1a1fd3f3a24c by blanchet:
prove 'set' property backward
The file was modified src/HOL/Tools/BNF/bnf_def.ML (diff)
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)
The file was modified src/HOL/Tools/BNF/bnf_fp_util.ML (diff)
The file was modified src/HOL/Tools/BNF/bnf_util.ML (diff)