src/HOL/Tools/inductive.ML
changeset 59725 e5dc7e7744f0
parent 59642 929984c529d3
child 59845 fafb4d12c307