# HG changeset patch
# User haftmann
# Date 1285597176 -7200
# Node ID 7aef0e4a3aac442a00eb19681a357ef2ce153f8b
# Parent  832c42be723e09933bc884376c0bf73bc601eede
combine quote and typewriter tag

diff -r 832c42be723e -r 7aef0e4a3aac doc-src/Classes/Thy/Classes.thy
--- a/doc-src/Classes/Thy/Classes.thy	Mon Sep 27 14:13:22 2010 +0200
+++ b/doc-src/Classes/Thy/Classes.thy	Mon Sep 27 16:19:36 2010 +0200
@@ -601,14 +601,14 @@
   \noindent This maps to Haskell as follows:
 *}
 (*<*)code_include %invisible Haskell "Natural" -(*>*)
-text %quote %typewriter {*
+text %quotetypewriter {*
   @{code_stmts example (Haskell)}
 *}
 
 text {*
   \noindent The code in SML has explicit dictionary passing:
 *}
-text %quote %typewriter {*
+text %quotetypewriter {*
   @{code_stmts example (SML)}
 *}
 
@@ -617,7 +617,7 @@
   \noindent In Scala, implicts are used as dictionaries:
 *}
 (*<*)code_include %invisible Scala "Natural" -(*>*)
-text %quote %typewriter {*
+text %quotetypewriter {*
   @{code_stmts example (Scala)}
 *}
 
diff -r 832c42be723e -r 7aef0e4a3aac doc-src/Classes/Thy/document/Classes.tex
--- a/doc-src/Classes/Thy/document/Classes.tex	Mon Sep 27 14:13:22 2010 +0200
+++ b/doc-src/Classes/Thy/document/Classes.tex	Mon Sep 27 16:19:36 2010 +0200
@@ -1123,11 +1123,11 @@
 %
 \endisadeliminvisible
 %
-\isadelimtypewriter
+\isadelimquotetypewriter
 %
-\endisadelimtypewriter
+\endisadelimquotetypewriter
 %
-\isatagtypewriter
+\isatagquotetypewriter
 %
 \begin{isamarkuptext}%
 module\ Example\ where\ {\isacharbraceleft}\isanewline
@@ -1195,23 +1195,23 @@
 \end{isamarkuptext}%
 \isamarkuptrue%
 %
-\endisatagtypewriter
-{\isafoldtypewriter}%
+\endisatagquotetypewriter
+{\isafoldquotetypewriter}%
 %
-\isadelimtypewriter
+\isadelimquotetypewriter
 %
-\endisadelimtypewriter
+\endisadelimquotetypewriter
 %
 \begin{isamarkuptext}%
 \noindent The code in SML has explicit dictionary passing:%
 \end{isamarkuptext}%
 \isamarkuptrue%
 %
-\isadelimtypewriter
+\isadelimquotetypewriter
 %
-\endisadelimtypewriter
+\endisadelimquotetypewriter
 %
-\isatagtypewriter
+\isatagquotetypewriter
 %
 \begin{isamarkuptext}%
 structure\ Example\ {\isacharcolon}\ sig\isanewline
@@ -1295,12 +1295,12 @@
 \end{isamarkuptext}%
 \isamarkuptrue%
 %
-\endisatagtypewriter
-{\isafoldtypewriter}%
+\endisatagquotetypewriter
+{\isafoldquotetypewriter}%
 %
-\isadelimtypewriter
+\isadelimquotetypewriter
 %
-\endisadelimtypewriter
+\endisadelimquotetypewriter
 %
 \begin{isamarkuptext}%
 \noindent In Scala, implicts are used as dictionaries:%
@@ -1320,11 +1320,11 @@
 %
 \endisadeliminvisible
 %
-\isadelimtypewriter
+\isadelimquotetypewriter
 %
-\endisadelimtypewriter
+\endisadelimquotetypewriter
 %
-\isatagtypewriter
+\isatagquotetypewriter
 %
 \begin{isamarkuptext}%
 object\ Example\ {\isacharbraceleft}\isanewline
@@ -1398,12 +1398,12 @@
 \end{isamarkuptext}%
 \isamarkuptrue%
 %
-\endisatagtypewriter
-{\isafoldtypewriter}%
+\endisatagquotetypewriter
+{\isafoldquotetypewriter}%
 %
-\isadelimtypewriter
+\isadelimquotetypewriter
 %
-\endisadelimtypewriter
+\endisadelimquotetypewriter
 %
 \isamarkupsubsection{Inspecting the type class universe%
 }