src/HOL/document/root.tex
changeset 78665 b0ddfa5b9ddc
parent 73595 aece5cc9efb7
equal deleted inserted replaced
78664:d052d61da398 78665:b0ddfa5b9ddc