13 \newcommand{\isastylescript}{\UNDEF} |
13 \newcommand{\isastylescript}{\UNDEF} |
14 \newcommand{\isastyletext}{\normalsize\rm} |
14 \newcommand{\isastyletext}{\normalsize\rm} |
15 \newcommand{\isastyletxt}{\rm} |
15 \newcommand{\isastyletxt}{\rm} |
16 \newcommand{\isastylecmt}{\rm} |
16 \newcommand{\isastylecmt}{\rm} |
17 |
17 |
|
18 \newcommand{\isaspacing}{\sfcode`\.1000 \sfcode 63 1000 \sfcode`\!1000 |
|
19 \sfcode`\:1000 \sfcode`\;1000 \sfcode`\,1000} |
|
20 |
18 %symbol markup -- \emph achieves decent spacing via italic corrections |
21 %symbol markup -- \emph achieves decent spacing via italic corrections |
19 \newcommand{\isamath}[1]{\emph{$#1$}} |
22 \newcommand{\isamath}[1]{\emph{$#1$}} |
20 \newcommand{\isatext}[1]{\emph{#1}} |
23 \newcommand{\isatext}[1]{\emph{#1}} |
21 \DeclareRobustCommand{\isascriptstyle}{\def\isamath##1{##1}\def\isatext##1{\mbox{\frenchspacing\isastylescript##1}}} |
24 \DeclareRobustCommand{\isascriptstyle}{\def\isamath##1{##1}\def\isatext##1{\mbox{\isaspacing\isastylescript##1}}} |
22 \newcommand{\isactrlsub}[1]{\emph{\isascriptstyle${}\sb{#1}$}} |
25 \newcommand{\isactrlsub}[1]{\emph{\isascriptstyle${}\sb{#1}$}} |
23 \newcommand{\isactrlsup}[1]{\emph{\isascriptstyle${}\sp{#1}$}} |
26 \newcommand{\isactrlsup}[1]{\emph{\isascriptstyle${}\sp{#1}$}} |
24 \newcommand{\isactrlisub}[1]{\emph{\isascriptstyle${}\sb{#1}$}} |
27 \newcommand{\isactrlisub}[1]{\emph{\isascriptstyle${}\sb{#1}$}} |
25 \newcommand{\isactrlisup}[1]{\emph{\isascriptstyle${}\sp{#1}$}} |
28 \newcommand{\isactrlisup}[1]{\emph{\isascriptstyle${}\sp{#1}$}} |
26 \DeclareRobustCommand{\isactrlbsub}{\emph\bgroup\math{}\sb\bgroup\mbox\bgroup\frenchspacing\isastylescript} |
29 \DeclareRobustCommand{\isactrlbsub}{\emph\bgroup\math{}\sb\bgroup\mbox\bgroup\isaspacing\isastylescript} |
27 \DeclareRobustCommand{\isactrlesub}{\egroup\egroup\endmath\egroup} |
30 \DeclareRobustCommand{\isactrlesub}{\egroup\egroup\endmath\egroup} |
28 \DeclareRobustCommand{\isactrlbsup}{\emph\bgroup\math{}\sp\bgroup\mbox\bgroup\frenchspacing\isastylescript} |
31 \DeclareRobustCommand{\isactrlbsup}{\emph\bgroup\math{}\sp\bgroup\mbox\bgroup\isaspacing\isastylescript} |
29 \DeclareRobustCommand{\isactrlesup}{\egroup\egroup\endmath\egroup} |
32 \DeclareRobustCommand{\isactrlesup}{\egroup\egroup\endmath\egroup} |
30 \newcommand{\isactrlbold}[1]{{\bfseries\upshape\boldmath#1}} |
33 \newcommand{\isactrlbold}[1]{{\bfseries\upshape\boldmath#1}} |
31 \newcommand{\isactrlloc}[1]{{\bfseries\upshape\boldmath#1}} |
34 \newcommand{\isactrlloc}[1]{{\bfseries\upshape\boldmath#1}} |
32 |
35 |
33 \newenvironment{isaantiq}{{\isacharat\isacharbraceleft}}{{\isacharbraceright}} |
36 \newenvironment{isaantiq}{{\isacharat\isacharbraceleft}}{{\isacharbraceright}} |
38 |
41 |
39 \newenvironment{isabellebody}{% |
42 \newenvironment{isabellebody}{% |
40 \isamarkuptrue\par% |
43 \isamarkuptrue\par% |
41 \isa@parindent\parindent\parindent0pt% |
44 \isa@parindent\parindent\parindent0pt% |
42 \isa@parskip\parskip\parskip0pt% |
45 \isa@parskip\parskip\parskip0pt% |
43 \frenchspacing\isastyle}{\par} |
46 \isaspacing\isastyle}{\par} |
44 |
47 |
45 \newenvironment{isabelle} |
48 \newenvironment{isabelle} |
46 {\begin{trivlist}\begin{isabellebody}\item\relax} |
49 {\begin{trivlist}\begin{isabellebody}\item\relax} |
47 {\end{isabellebody}\end{trivlist}} |
50 {\end{isabellebody}\end{trivlist}} |
48 |
51 |
49 \newcommand{\isa}[1]{\emph{\frenchspacing\isastyleminor #1}} |
52 \newcommand{\isa}[1]{\emph{\isaspacing\isastyleminor #1}} |
50 |
53 |
51 \newcommand{\isaindent}[1]{\hphantom{#1}} |
54 \newcommand{\isaindent}[1]{\hphantom{#1}} |
52 \newcommand{\isanewline}{\mbox{}\par\mbox{}} |
55 \newcommand{\isanewline}{\mbox{}\par\mbox{}} |
53 \newcommand{\isasep}{} |
56 \newcommand{\isasep}{} |
54 \newcommand{\isadigit}[1]{#1} |
57 \newcommand{\isadigit}[1]{#1} |