# HG changeset patch
# User wenzelm
# Date 1512592226 -3600
# Node ID d1ace598c026159670b4e88853a242cb4fd225ca
# Parent  ecbd8ff928c56c54b88196c1358bf42cd59d4006
more default tags;

diff -r ecbd8ff928c5 -r d1ace598c026 lib/texinputs/isabelle.sty
--- a/lib/texinputs/isabelle.sty	Wed Dec 06 21:01:01 2017 +0100
+++ b/lib/texinputs/isabelle.sty	Wed Dec 06 21:30:26 2017 +0100
@@ -259,5 +259,7 @@
 \isakeeptag{ML}
 \isakeeptag{visible}
 \isadroptag{invisible}
+\isakeeptag{important}
+\isakeeptag{unimportant}
 
 \IfFileExists{isabelletags.sty}{\usepackage{isabelletags}}{}
diff -r ecbd8ff928c5 -r d1ace598c026 src/Doc/System/Presentation.thy
--- a/src/Doc/System/Presentation.thy	Wed Dec 06 21:01:01 2017 +0100
+++ b/src/Doc/System/Presentation.thy	Wed Dec 06 21:30:26 2017 +0100
@@ -182,9 +182,9 @@
   pairs: ``\<^verbatim>\<open>+\<close>\<open>foo\<close>'' (or just ``\<open>foo\<close>'') means to keep, ``\<^verbatim>\<open>-\<close>\<open>foo\<close>'' to
   drop, and ``\<^verbatim>\<open>/\<close>\<open>foo\<close>'' to fold text tagged as \<open>foo\<close>. The builtin default is
   equivalent to the tag specification
-  ``\<^verbatim>\<open>+document,+theory,+proof,+ML,+visible,-invisible\<close>''; see also the {\LaTeX} macros
-  \<^verbatim>\<open>\isakeeptag\<close>, \<^verbatim>\<open>\isadroptag\<close>, and \<^verbatim>\<open>\isafoldtag\<close>, in
-  \<^file>\<open>~~/lib/texinputs/isabelle.sty\<close>.
+  ``\<^verbatim>\<open>+document,+theory,+proof,+ML,+visible,-invisible,+important,+unimportant\<close>'';
+  see also the {\LaTeX} macros \<^verbatim>\<open>\isakeeptag\<close>, \<^verbatim>\<open>\isadroptag\<close>, and
+  \<^verbatim>\<open>\isafoldtag\<close>, in \<^file>\<open>~~/lib/texinputs/isabelle.sty\<close>.
 
   \<^medskip>
   Document preparation requires a \<^verbatim>\<open>document\<close> directory within the session