src/HOL/Induct/ROOT.ML
changeset 48003 1d11af40b106
parent 39616 8052101883c3