src/HOL/Induct/document/root.tex
changeset 76371 1ac2416e8432
parent 73404 299f6a8faccc
child 77036 d0151eb9ecb0