src/HOL/Induct/ROOT.ML
changeset 41953 994d088fbfbc
parent 39616 8052101883c3