\isabellestyleit: proper \isacharbackslash;
support for tagged regions: \isakeeptag, \isadroptag, \isafoldtag -- depends on plain TeX version of comment.sty;

--- a/lib/texinputs/isabelle.sty	Tue Aug 16 13:42:17 2005 +0200
+++ b/lib/texinputs/isabelle.sty	Tue Aug 16 13:42:18 2005 +0200
@@ -149,6 +149,7 @@
 \renewcommand{\isachargreater}{\isamath{>}}%
 \renewcommand{\isacharat}{\isamath{@}}%
 \renewcommand{\isacharbrackleft}{\isamath{[}}%
+\renewcommand{\isacharbackslash}{\isamath{\backslash}}%
 \renewcommand{\isacharbrackright}{\isamath{]}}%
 \renewcommand{\isacharunderscore}{\mbox{-}}%
 \renewcommand{\isacharbraceleft}{\isamath{\{}}%
@@ -163,3 +164,28 @@
 \renewcommand{\isastyleminor}{\sl}%
 \renewcommand{\isastylescript}{\footnotesize\sl}%
 }
+
+
+% tagged regions
+
+%plain TeX version of comment package -- much faster!
+\let\isafmtname\fmtname\def\fmtname{plain}
+\usepackage{comment}
+\let\fmtname\isafmtname
+
+\newcommand{\isafold}[1]{\emph{$\langle\mathord{\mathit{#1}}\rangle$}}
+
+\newcommand{\isakeeptag}[1]%
+{\includecomment{isadelim#1}\includecomment{isatag#1}\csarg\def{isafold#1}{}}
+\newcommand{\isadroptag}[1]%
+{\excludecomment{isadelim#1}\excludecomment{isatag#1}\csarg\def{isafold#1}{}}
+\newcommand{\isafoldtag}[1]%
+{\includecomment{isadelim#1}\excludecomment{isatag#1}\csarg\def{isafold#1}{\isafold{#1}}}
+
+\isakeeptag{theory}
+\isakeeptag{proof}
+\isakeeptag{ML}
+\isakeeptag{visible}
+\isadroptag{invisible}
+
+\IfFileExists{isabelletags.sty}{\usepackage{isabelletags}}{}