src/HOL/Induct/ROOT.ML
changeset 43037 ade5c84f860f
parent 39616 8052101883c3