src/HOL/Tools/inductive.ML
changeset 63260 0edec65d0633
parent 63180 ddfd021884b4
child 63285 e9c777bfd78c