doc-src/IsarRef/Thy/document/Inner_Syntax.tex
Sat, 08 May 2010 19:53:11 +0200 wenzelm discontinued Pretty.setdepth, which appears to be largely unused, but can disrupt important markup if enabled accidentally;
less more (0) -10 -1 tip