Skip to content
Success

Changes

Summary

  1. refactored induction principle generation code, for reuse for nonuniform datatypes
Changeset 64576:ce8802dc3145 by blanchet:
refactored induction principle generation code, for reuse for nonuniform datatypes
The file was modified src/HOL/Tools/BNF/bnf_fp_def_sugar.ML (diff)