src/HOL/Induct/document/root.tex
changeset 75176 e3388efdacd7
parent 73404 299f6a8faccc
child 77036 d0151eb9ecb0