src/HOL/Induct/ROOT.ML
changeset 47356 19fb95255ec9
parent 39616 8052101883c3