equal
deleted
inserted
replaced
37 {\begin{trivlist}\begin{isabellebody}\item\relax} |
37 {\begin{trivlist}\begin{isabellebody}\item\relax} |
38 {\end{isabellebody}\end{trivlist}} |
38 {\end{isabellebody}\end{trivlist}} |
39 |
39 |
40 \newcommand{\isa}[1]{\emph{\isastyleminor #1}} |
40 \newcommand{\isa}[1]{\emph{\isastyleminor #1}} |
41 |
41 |
|
42 \newcommand{\isaindent}[1]{\hphantom{#1}} |
42 \newcommand{\isanewline}{\mbox{}\\\mbox{}} |
43 \newcommand{\isanewline}{\mbox{}\\\mbox{}} |
43 \newcommand{\isadigit}[1]{#1} |
44 \newcommand{\isadigit}[1]{#1} |
44 |
45 |
45 \chardef\isacharbang=`\! |
46 \chardef\isacharbang=`\! |
46 \chardef\isachardoublequote=`\" |
47 \chardef\isachardoublequote=`\" |