# HG changeset patch
# User wenzelm
# Date 1235666556 -3600
# Node ID 5ea17e90b08a1e82b681696bde5a3e6233de2c28
# Parent  01a87bc13415afa09d9543d1315b2ba01fa24029
isabelle document: adapted (postulated) defaults for tags to actual isabelle.sty;

diff -r 01a87bc13415 -r 5ea17e90b08a doc-src/System/Thy/Presentation.thy
--- a/doc-src/System/Thy/Presentation.thy	Thu Feb 26 16:59:04 2009 +0100
+++ b/doc-src/System/Thy/Presentation.thy	Thu Feb 26 17:42:36 2009 +0100
@@ -654,7 +654,7 @@
   "-"}@{text foo}'' to drop, and ``@{verbatim "/"}@{text foo}'' to
   fold text tagged as @{text foo}.  The builtin default is equivalent
   to the tag specification ``@{verbatim
-  "/theory,/proof,/ML,+visible,-invisible"}''; see also the {\LaTeX}
+  "+theory,+proof,+ML,+visible,-invisible"}''; see also the {\LaTeX}
   macros @{verbatim "\\isakeeptag"}, @{verbatim "\\isadroptag"}, and
   @{verbatim "\\isafoldtag"}, in @{"file"
   "~~/lib/texinputs/isabelle.sty"}.