doc-src/IsarRef/Thy/Inner_Syntax.thy
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