src/HOL/Induct/document/root.tex
changeset 80023 c43a51fde4f5
parent 77036 d0151eb9ecb0
equal deleted inserted replaced
80022:77e605c66797 80023:c43a51fde4f5