src/HOL/Induct/ROOT.ML
changeset 16633 208ebc9311f2
parent 15172 73069e033a0b
child 17598 7540ccd2b445