Skip to content
Success

Changes

Summary

  1. export ML functions (towards nonuniform codatatypes) + signature tuning
Changeset 64637:a15785625f7c by blanchet:
export ML functions (towards nonuniform codatatypes) + signature tuning
The file was modified src/HOL/Tools/BNF/bnf_fp_def_sugar.ML (diff)
The file was modified src/HOL/Tools/BNF/bnf_fp_n2m_sugar.ML (diff)
The file was modified src/HOL/Tools/BNF/bnf_gfp_grec_sugar.ML (diff)