src/Doc/System/Presentation.thy
changeset 67151 d1ace598c026
parent 67139 8fe0aba577af
child 67176 13b5c3ff1954
     1.1 --- a/src/Doc/System/Presentation.thy	Tue Dec 05 15:55:14 2017 +0100
     1.2 +++ b/src/Doc/System/Presentation.thy	Wed Dec 06 21:30:26 2017 +0100
     1.3 @@ -182,9 +182,9 @@
     1.4    pairs: ``\<^verbatim>\<open>+\<close>\<open>foo\<close>'' (or just ``\<open>foo\<close>'') means to keep, ``\<^verbatim>\<open>-\<close>\<open>foo\<close>'' to
     1.5    drop, and ``\<^verbatim>\<open>/\<close>\<open>foo\<close>'' to fold text tagged as \<open>foo\<close>. The builtin default is
     1.6    equivalent to the tag specification
     1.7 -  ``\<^verbatim>\<open>+document,+theory,+proof,+ML,+visible,-invisible\<close>''; see also the {\LaTeX} macros
     1.8 -  \<^verbatim>\<open>\isakeeptag\<close>, \<^verbatim>\<open>\isadroptag\<close>, and \<^verbatim>\<open>\isafoldtag\<close>, in
     1.9 -  \<^file>\<open>~~/lib/texinputs/isabelle.sty\<close>.
    1.10 +  ``\<^verbatim>\<open>+document,+theory,+proof,+ML,+visible,-invisible,+important,+unimportant\<close>'';
    1.11 +  see also the {\LaTeX} macros \<^verbatim>\<open>\isakeeptag\<close>, \<^verbatim>\<open>\isadroptag\<close>, and
    1.12 +  \<^verbatim>\<open>\isafoldtag\<close>, in \<^file>\<open>~~/lib/texinputs/isabelle.sty\<close>.
    1.13  
    1.14    \<^medskip>
    1.15    Document preparation requires a \<^verbatim>\<open>document\<close> directory within the session