src/HOL/Induct/document/root.tex
changeset 76371 1ac2416e8432
parent 73404 299f6a8faccc
child 77036 d0151eb9ecb0
equal deleted inserted replaced
76370:9bd948666e8a 76371:1ac2416e8432