# HG changeset patch
# User haftmann
# Date 1285241101 -7200
# Node ID 86595d7b59b5fd6361cf9fe859e976a1b8255bfb
# Parent  6381d18507ef2da6a01b316095cc9140d48c06f7
reverted cs 5aced2f43837 -- no need for hardwired latex command here

diff -r 6381d18507ef -r 86595d7b59b5 lib/texinputs/isabelle.sty
--- a/lib/texinputs/isabelle.sty	Thu Sep 23 13:23:22 2010 +0200
+++ b/lib/texinputs/isabelle.sty	Thu Sep 23 13:25:01 2010 +0200
@@ -46,8 +46,6 @@
 {\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}}