\\isatypewrite now part of isabelle latex style
authorhaftmann
Mon, 20 Sep 2010 09:19:13 +0200
changeset 39538 5aced2f43837
parent 39537 41afe7124aa6
child 39539 90a74f43174d
\\isatypewrite now part of isabelle latex style
doc-src/Classes/style.sty
doc-src/Codegen/style.sty
lib/texinputs/isabelle.sty
--- a/doc-src/Classes/style.sty	Mon Sep 20 08:53:37 2010 +0200
+++ b/doc-src/Classes/style.sty	Mon Sep 20 09:19:13 2010 +0200
@@ -17,9 +17,6 @@
 %% typographic conventions
 \newcommand{\qt}[1]{``{#1}''}
 
-%% verbatim text
-\newcommand{\isatypewriter}{\fontsize{9pt}{0pt}\tt\renewcommand{\baselinestretch}{1}\setlength{\baselineskip}{9pt}}
-
 %% quote environment
 \isakeeptag{quote}
 \renewenvironment{quote}
--- a/doc-src/Codegen/style.sty	Mon Sep 20 08:53:37 2010 +0200
+++ b/doc-src/Codegen/style.sty	Mon Sep 20 09:19:13 2010 +0200
@@ -17,9 +17,6 @@
 \newcommand{\qt}[1]{``{#1}''}
 \newcommand{\ditem}[1]{\item[\isastyletext #1]}
 
-%% verbatim text
-\newcommand{\isatypewriter}{\fontsize{9pt}{0pt}\tt\renewcommand{\baselinestretch}{1}\setlength{\baselineskip}{9pt}}
-
 %% quote environment
 \isakeeptag{quote}
 \renewenvironment{quote}
--- a/lib/texinputs/isabelle.sty	Mon Sep 20 08:53:37 2010 +0200
+++ b/lib/texinputs/isabelle.sty	Mon Sep 20 09:19:13 2010 +0200
@@ -46,6 +46,8 @@
 {\begin{trivlist}\begin{isabellebody}\item\relax}
 {\end{isabellebody}\end{trivlist}}
 
+\newcommand{\isatypewriter}{\fontsize{9pt}{0pt}\tt\renewcommand{\baselinestretch}{1}\setlength{\baselineskip}{9pt}}
+
 \newcommand{\isa}[1]{\emph{\isastyleminor #1}}
 
 \newcommand{\isaindent}[1]{\hphantom{#1}}