src/HOL/Induct/ROOT.ML
changeset 46725 d34ec0512dfb
parent 39616 8052101883c3