Skip to content
Success

Changes

Summary

  1. generalized ML function (towards nonuniform datatypes)
  2. generalized ML function (towards nonuniform datatypes)
Changeset 64627:8d7cb22482e3 by blanchet:
generalized ML function (towards nonuniform datatypes)
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_gfp_grec.ML (diff)
The file was modified src/HOL/Tools/BNF/bnf_gfp_grec_sugar.ML (diff)
The file was modified src/HOL/Tools/BNF/bnf_gfp_grec_sugar_util.ML (diff)
The file was modified src/HOL/Tools/BNF/bnf_gfp_rec_sugar.ML (diff)
The file was modified src/HOL/Tools/BNF/bnf_lfp_countable.ML (diff)
The file was modified src/HOL/Tools/BNF/bnf_lfp_rec_sugar_more.ML (diff)
Changeset 64626:f6d0578b46c9 by blanchet:
generalized ML function (towards nonuniform datatypes)
The file was modified src/HOL/Tools/BNF/bnf_fp_def_sugar.ML (diff)