# HG changeset patch
# User haftmann
# Date 1284967153 -7200
# Node ID 5aced2f43837a3850f51823da90cd26763573c54
# Parent  41afe7124aa6d720c9d8ddc634b84fc78b32dda3
\\isatypewrite now part of isabelle latex style

diff -r 41afe7124aa6 -r 5aced2f43837 doc-src/Classes/style.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}
diff -r 41afe7124aa6 -r 5aced2f43837 doc-src/Codegen/style.sty
--- 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}
diff -r 41afe7124aa6 -r 5aced2f43837 lib/texinputs/isabelle.sty
--- 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}}