src/HOL/Tools/typedef_codegen.ML
changeset 28524 644b62cf678f
parent 27398 768da1da59d6
child 28537 1e84256d1a8a