Skip to content
[Jenkins]Jenkins
log in
Success

Changes

Summary

  1. merge
  2. avoid duplicate mixfix messages in '(co)datatype' type name
  3. generalize code to avoid making assumptions about type variable names
  4. intermediate definitions and caching in n2m to keep terms small
  5. n2m operates on (un)folds
Changeset 63049:2cc4e85b46d4 by blanchet:
merge
Changeset 63048:1836456b7d82 by blanchet:
avoid duplicate mixfix messages in '(co)datatype' type name
The file was modified src/HOL/Tools/BNF/bnf_fp_def_sugar.ML (diff)
Changeset 63047:2146553e96c6 by blanchet:
generalize code to avoid making assumptions about type variable names
The file was modified src/HOL/Tools/BNF/bnf_lfp_compat.ML (diff)
Changeset 63046:8053ef5a0174 by traytel:
intermediate definitions and caching in n2m to keep terms small
The file was modified src/HOL/BNF_Fixpoint_Base.thy (diff)
The file was modified src/HOL/Tools/BNF/bnf_fp_n2m.ML (diff)
The file was modified src/HOL/Tools/BNF/bnf_fp_n2m_tactics.ML (diff)
Changeset 63045:c50c764aab10 by traytel:
n2m operates on (un)folds
The file was modified src/HOL/Basic_BNF_LFPs.thy (diff)
The file was modified src/HOL/Tools/BNF/bnf_fp_n2m.ML (diff)
The file was modified src/HOL/Tools/BNF/bnf_fp_n2m_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_fp_util_tactics.ML (diff)
The file was modified src/HOL/Tools/BNF/bnf_gfp.ML (diff)
The file was modified src/HOL/Tools/BNF/bnf_lfp.ML (diff)
The file was modified src/HOL/Tools/BNF/bnf_lfp_basic_sugar.ML (diff)