src/HOL/Induct/ROOT.ML
changeset 12887 d25b43743e10
parent 11641 0c248bed5225
child 13075 d3e1d554cd6d