1.1 --- a/NEWS	Sun May 01 16:56:50 2011 +0200
     1.2 +++ b/NEWS	Sun May 01 17:13:44 2011 +0200
     1.3 @@ -83,6 +83,12 @@
     1.4  
     1.5  *** Document preparation ***
     1.6  
     1.7 +* Localized \isabellestyle switch can be used within blocks or groups
     1.8 +like this:
     1.9 +
    1.10 +  \isabellestyle{it}  %preferred default
    1.11 +  {\isabellestylett @{text "typewriter stuff"}}
    1.12 +
    1.13  * New term style "isub" as ad-hoc conversion of variables x1, y23 into
    1.14  subscripted form x\<^isub>1, y\<^isub>2\<^isub>3.
    1.15  

     2.1 --- a/lib/texinputs/isabelle.sty	Sun May 01 16:56:50 2011 +0200
     2.2 +++ b/lib/texinputs/isabelle.sty	Sun May 01 17:13:44 2011 +0200
     2.3 @@ -129,67 +129,68 @@
     2.4  \def\isabellestyle#1{\csname isabellestyle#1\endcsname}
     2.5  
     2.6  \newcommand{\isabellestyledefault}{%
     2.7 -\renewcommand{\isastyle}{\small\tt\slshape}%
     2.8 -\renewcommand{\isastyleminor}{\small\tt\slshape}%
     2.9 -\renewcommand{\isastylescript}{\footnotesize\tt\slshape}%
    2.10 +\def\isastyle{\small\tt\slshape}%
    2.11 +\def\isastyleminor{\small\tt\slshape}%
    2.12 +\def\isastylescript{\footnotesize\tt\slshape}%
    2.13  \isachardefaults%
    2.14  }
    2.15  \isabellestyledefault
    2.16  
    2.17  \newcommand{\isabellestylett}{%
    2.18 -\renewcommand{\isastyle}{\small\tt}%
    2.19 -\renewcommand{\isastyleminor}{\small\tt}%
    2.20 -\renewcommand{\isastylescript}{\footnotesize\tt}%
    2.21 +\def\isastyle{\small\tt}%
    2.22 +\def\isastyleminor{\small\tt}%
    2.23 +\def\isastylescript{\footnotesize\tt}%
    2.24  \isachardefaults%
    2.25  }
    2.26  
    2.27  \newcommand{\isabellestyleit}{%
    2.28 -\renewcommand{\isastyle}{\small\it}%
    2.29 -\renewcommand{\isastyleminor}{\it}%
    2.30 -\renewcommand{\isastylescript}{\footnotesize\it}%
    2.31 -\renewcommand{\isacharunderscorekeyword}{\mbox{-}}%
    2.32 -\renewcommand{\isacharbang}{\isamath{!}}%
    2.33 -\renewcommand{\isachardoublequote}{\isanil}%
    2.34 -\renewcommand{\isachardoublequoteopen}{\isanil}%
    2.35 -\renewcommand{\isachardoublequoteclose}{\isanil}%
    2.36 -\renewcommand{\isacharhash}{\isamath{\#}}%
    2.37 -\renewcommand{\isachardollar}{\isamath{\$}}%
    2.38 -\renewcommand{\isacharpercent}{\isamath{\%}}%
    2.39 -\renewcommand{\isacharampersand}{\isamath{\&}}%
    2.40 -\renewcommand{\isacharprime}{\isamath{\mskip2mu{'}\mskip-2mu}}%
    2.41 -\renewcommand{\isacharparenleft}{\isamath{(}}%
    2.42 -\renewcommand{\isacharparenright}{\isamath{)}}%
    2.43 -\renewcommand{\isacharasterisk}{\isamath{*}}%
    2.44 -\renewcommand{\isacharplus}{\isamath{+}}%
    2.45 -\renewcommand{\isacharcomma}{\isamath{\mathord,}}%
    2.46 -\renewcommand{\isacharminus}{\isamath{-}}%
    2.47 -\renewcommand{\isachardot}{\isamath{\mathord.}}%
    2.48 -\renewcommand{\isacharslash}{\isamath{/}}%
    2.49 -\renewcommand{\isacharcolon}{\isamath{\mathord:}}%
    2.50 -\renewcommand{\isacharsemicolon}{\isamath{\mathord;}}%
    2.51 -\renewcommand{\isacharless}{\isamath{<}}%
    2.52 -\renewcommand{\isacharequal}{\isamath{=}}%
    2.53 -\renewcommand{\isachargreater}{\isamath{>}}%
    2.54 -\renewcommand{\isacharat}{\isamath{@}}%
    2.55 -\renewcommand{\isacharbrackleft}{\isamath{[}}%
    2.56 -\renewcommand{\isacharbackslash}{\isamath{\backslash}}%
    2.57 -\renewcommand{\isacharbrackright}{\isamath{]}}%
    2.58 -\renewcommand{\isacharunderscore}{\mbox{-}}%
    2.59 -\renewcommand{\isacharbraceleft}{\isamath{\{}}%
    2.60 -\renewcommand{\isacharbar}{\isamath{\mid}}%
    2.61 -\renewcommand{\isacharbraceright}{\isamath{\}}}%
    2.62 -\renewcommand{\isachartilde}{\isamath{{}\sp{\sim}}}%
    2.63 -\renewcommand{\isacharbackquoteopen}{\isatext{\raise.3ex\hbox{$\scriptscriptstyle\langle$}}}%
    2.64 -\renewcommand{\isacharbackquoteclose}{\isatext{\raise.3ex\hbox{$\scriptscriptstyle\rangle$}}}%
    2.65 -\renewcommand{\isacharverbatimopen}{\isamath{\langle\!\langle}}%
    2.66 -\renewcommand{\isacharverbatimclose}{\isamath{\rangle\!\rangle}}%
    2.67 +\def\isastyle{\small\it}%
    2.68 +\def\isastyleminor{\it}%
    2.69 +\def\isastylescript{\footnotesize\it}%
    2.70 +\isachardefaults%
    2.71 +\def\isacharunderscorekeyword{\mbox{-}}%
    2.72 +\def\isacharbang{\isamath{!}}%
    2.73 +\def\isachardoublequote{\isanil}%
    2.74 +\def\isachardoublequoteopen{\isanil}%
    2.75 +\def\isachardoublequoteclose{\isanil}%
    2.76 +\def\isacharhash{\isamath{\#}}%
    2.77 +\def\isachardollar{\isamath{\$}}%
    2.78 +\def\isacharpercent{\isamath{\%}}%
    2.79 +\def\isacharampersand{\isamath{\&}}%
    2.80 +\def\isacharprime{\isamath{\mskip2mu{'}\mskip-2mu}}%
    2.81 +\def\isacharparenleft{\isamath{(}}%
    2.82 +\def\isacharparenright{\isamath{)}}%
    2.83 +\def\isacharasterisk{\isamath{*}}%
    2.84 +\def\isacharplus{\isamath{+}}%
    2.85 +\def\isacharcomma{\isamath{\mathord,}}%
    2.86 +\def\isacharminus{\isamath{-}}%
    2.87 +\def\isachardot{\isamath{\mathord.}}%
    2.88 +\def\isacharslash{\isamath{/}}%
    2.89 +\def\isacharcolon{\isamath{\mathord:}}%
    2.90 +\def\isacharsemicolon{\isamath{\mathord;}}%
    2.91 +\def\isacharless{\isamath{<}}%
    2.92 +\def\isacharequal{\isamath{=}}%
    2.93 +\def\isachargreater{\isamath{>}}%
    2.94 +\def\isacharat{\isamath{@}}%
    2.95 +\def\isacharbrackleft{\isamath{[}}%
    2.96 +\def\isacharbackslash{\isamath{\backslash}}%
    2.97 +\def\isacharbrackright{\isamath{]}}%
    2.98 +\def\isacharunderscore{\mbox{-}}%
    2.99 +\def\isacharbraceleft{\isamath{\{}}%
   2.100 +\def\isacharbar{\isamath{\mid}}%
   2.101 +\def\isacharbraceright{\isamath{\}}}%
   2.102 +\def\isachartilde{\isamath{{}\sp{\sim}}}%
   2.103 +\def\isacharbackquoteopen{\isatext{\raise.3ex\hbox{$\scriptscriptstyle\langle$}}}%
   2.104 +\def\isacharbackquoteclose{\isatext{\raise.3ex\hbox{$\scriptscriptstyle\rangle$}}}%
   2.105 +\def\isacharverbatimopen{\isamath{\langle\!\langle}}%
   2.106 +\def\isacharverbatimclose{\isamath{\rangle\!\rangle}}%
   2.107  }
   2.108  
   2.109  \newcommand{\isabellestylesl}{%
   2.110  \isabellestyleit%
   2.111 -\renewcommand{\isastyle}{\small\sl}%
   2.112 -\renewcommand{\isastyleminor}{\sl}%
   2.113 -\renewcommand{\isastylescript}{\footnotesize\sl}%
   2.114 +\def\isastyle{\small\sl}%
   2.115 +\def\isastyleminor{\sl}%
   2.116 +\def\isastylescript{\footnotesize\sl}%
   2.117  }
   2.118  
   2.119