src/HOL/Induct/document/root.tex
changeset 13049 ce180e5b7fa0
parent 12185 54bd9aa3343d
child 61993 89206877f0ee
equal deleted inserted replaced
13048:8b2eb3b78cc3 13049:ce180e5b7fa0