src/HOL/Examples/document/root.tex
changeset 74596 55d4f8e1877f
parent 73404 299f6a8faccc
child 74889 7dbac7d3cdab
equal deleted inserted replaced
74595:71bafd70acbb 74596:55d4f8e1877f