# HG changeset patch
# User haftmann
# Date 1285570043 -7200
# Node ID d3f46f1ca1f1adae0bf0850c03695e9897a10987
# Parent  6542245db5c2961b0a71f8fb41d716be84bd73b6# Parent  94b1890e4e4a0be38d7dffb8654bb92e44ba9779
merged

diff -r 6542245db5c2 -r d3f46f1ca1f1 doc-src/Codegen/Thy/Adaptation.thy
--- a/doc-src/Codegen/Thy/Adaptation.thy	Sat Sep 25 10:32:14 2010 +0200
+++ b/doc-src/Codegen/Thy/Adaptation.thy	Mon Sep 27 08:47:23 2010 +0200
@@ -190,9 +190,9 @@
   "bool"}, we may use \qn{custom serialisations}:
 *}
 
-code_type %quotett bool
+code_type %quote %tt bool
   (SML "bool")
-code_const %quotett True and False and "op \<and>"
+code_const %quote %tt True and False and "op \<and>"
   (SML "true" and "false" and "_ andalso _")
 
 text {*
@@ -218,7 +218,7 @@
   precedences which may be used here:
 *}
 
-code_const %quotett "op \<and>"
+code_const %quote %tt "op \<and>"
   (SML infixl 1 "andalso")
 
 text %quote %typewriter {*
@@ -247,9 +247,9 @@
 code_const %invisible Pair
   (SML)
 (*>*)
-code_type %quotett prod
+code_type %quote %tt prod
   (SML infix 2 "*")
-code_const %quotett Pair
+code_const %quote %tt Pair
   (SML "!((_),/ (_))")
 
 text {*
@@ -283,10 +283,10 @@
   @{command_def code_class}) and its operation @{const [source] HOL.equal}
 *}
 
-code_class %quotett equal
+code_class %quote %tt equal
   (Haskell "Eq")
 
-code_const %quotett "HOL.equal"
+code_const %quote %tt "HOL.equal"
   (Haskell infixl 4 "==")
 
 text {*
@@ -307,7 +307,7 @@
 
 end %quote (*<*)
 
-(*>*) code_type %quotett bar
+(*>*) code_type %quote %tt bar
   (Haskell "Integer")
 
 text {*
@@ -316,7 +316,7 @@
   suppress this additional instance, use @{command_def "code_instance"}:
 *}
 
-code_instance %quotett bar :: equal
+code_instance %quote %tt bar :: equal
   (Haskell -)
 
 
@@ -328,10 +328,10 @@
   "code_include"} command:
 *}
 
-code_include %quotett Haskell "Errno"
+code_include %quote %tt Haskell "Errno"
 {*errno i = error ("Error number: " ++ show i)*}
 
-code_reserved %quotett Haskell Errno
+code_reserved %quote %tt Haskell Errno
 
 text {*
   \noindent Such named @{text include}s are then prepended to every
diff -r 6542245db5c2 -r d3f46f1ca1f1 doc-src/Codegen/Thy/Evaluation.thy
--- a/doc-src/Codegen/Thy/Evaluation.thy	Sat Sep 25 10:32:14 2010 +0200
+++ b/doc-src/Codegen/Thy/Evaluation.thy	Mon Sep 27 08:47:23 2010 +0200
@@ -206,7 +206,7 @@
 
 datatype %quote form = T | F | And form form | Or form form (*<*)
 
-(*>*) ML %quotett {*
+(*>*) ML %tt %quote {*
   fun eval_form @{code T} = true
     | eval_form @{code F} = false
     | eval_form (@{code And} (p, q)) =
diff -r 6542245db5c2 -r d3f46f1ca1f1 doc-src/Codegen/Thy/document/Adaptation.tex
--- a/doc-src/Codegen/Thy/document/Adaptation.tex	Sat Sep 25 10:32:14 2010 +0200
+++ b/doc-src/Codegen/Thy/document/Adaptation.tex	Mon Sep 27 08:47:23 2010 +0200
@@ -281,23 +281,23 @@
 \end{isamarkuptext}%
 \isamarkuptrue%
 %
-\isadelimquotett
+\isadelimtt
 %
-\endisadelimquotett
+\endisadelimtt
 %
-\isatagquotett
+\isatagtt
 \isacommand{code{\isacharunderscore}type}\isamarkupfalse%
 \ bool\isanewline
 \ \ {\isacharparenleft}SML\ {\isachardoublequoteopen}bool{\isachardoublequoteclose}{\isacharparenright}\isanewline
 \isacommand{code{\isacharunderscore}const}\isamarkupfalse%
 \ True\ \isakeyword{and}\ False\ \isakeyword{and}\ {\isachardoublequoteopen}op\ {\isasymand}{\isachardoublequoteclose}\isanewline
 \ \ {\isacharparenleft}SML\ {\isachardoublequoteopen}true{\isachardoublequoteclose}\ \isakeyword{and}\ {\isachardoublequoteopen}false{\isachardoublequoteclose}\ \isakeyword{and}\ {\isachardoublequoteopen}{\isacharunderscore}\ andalso\ {\isacharunderscore}{\isachardoublequoteclose}{\isacharparenright}%
-\endisatagquotett
-{\isafoldquotett}%
+\endisatagtt
+{\isafoldtt}%
 %
-\isadelimquotett
+\isadelimtt
 %
-\endisadelimquotett
+\endisadelimtt
 %
 \begin{isamarkuptext}%
 \noindent The \indexdef{}{command}{code\_type}\hypertarget{command.code-type}{\hyperlink{command.code-type}{\mbox{\isa{\isacommand{code{\isacharunderscore}type}}}}} command takes a type constructor
@@ -354,20 +354,20 @@
 \end{isamarkuptext}%
 \isamarkuptrue%
 %
-\isadelimquotett
+\isadelimtt
 %
-\endisadelimquotett
+\endisadelimtt
 %
-\isatagquotett
+\isatagtt
 \isacommand{code{\isacharunderscore}const}\isamarkupfalse%
 \ {\isachardoublequoteopen}op\ {\isasymand}{\isachardoublequoteclose}\isanewline
 \ \ {\isacharparenleft}SML\ \isakeyword{infixl}\ {\isadigit{1}}\ {\isachardoublequoteopen}andalso{\isachardoublequoteclose}{\isacharparenright}%
-\endisatagquotett
-{\isafoldquotett}%
+\endisatagtt
+{\isafoldtt}%
 %
-\isadelimquotett
+\isadelimtt
 %
-\endisadelimquotett
+\endisadelimtt
 %
 \isadelimtypewriter
 %
@@ -447,23 +447,23 @@
 %
 \endisadeliminvisible
 %
-\isadelimquotett
+\isadelimtt
 %
-\endisadelimquotett
+\endisadelimtt
 %
-\isatagquotett
+\isatagtt
 \isacommand{code{\isacharunderscore}type}\isamarkupfalse%
 \ prod\isanewline
 \ \ {\isacharparenleft}SML\ \isakeyword{infix}\ {\isadigit{2}}\ {\isachardoublequoteopen}{\isacharasterisk}{\isachardoublequoteclose}{\isacharparenright}\isanewline
 \isacommand{code{\isacharunderscore}const}\isamarkupfalse%
 \ Pair\isanewline
 \ \ {\isacharparenleft}SML\ {\isachardoublequoteopen}{\isacharbang}{\isacharparenleft}{\isacharparenleft}{\isacharunderscore}{\isacharparenright}{\isacharcomma}{\isacharslash}\ {\isacharparenleft}{\isacharunderscore}{\isacharparenright}{\isacharparenright}{\isachardoublequoteclose}{\isacharparenright}%
-\endisatagquotett
-{\isafoldquotett}%
+\endisatagtt
+{\isafoldtt}%
 %
-\isadelimquotett
+\isadelimtt
 %
-\endisadelimquotett
+\endisadelimtt
 %
 \begin{isamarkuptext}%
 \noindent The initial bang ``\verb|!|'' tells the serialiser
@@ -499,11 +499,11 @@
 \end{isamarkuptext}%
 \isamarkuptrue%
 %
-\isadelimquotett
+\isadelimtt
 %
-\endisadelimquotett
+\endisadelimtt
 %
-\isatagquotett
+\isatagtt
 \isacommand{code{\isacharunderscore}class}\isamarkupfalse%
 \ equal\isanewline
 \ \ {\isacharparenleft}Haskell\ {\isachardoublequoteopen}Eq{\isachardoublequoteclose}{\isacharparenright}\isanewline
@@ -511,12 +511,12 @@
 \isacommand{code{\isacharunderscore}const}\isamarkupfalse%
 \ {\isachardoublequoteopen}HOL{\isachardot}equal{\isachardoublequoteclose}\isanewline
 \ \ {\isacharparenleft}Haskell\ \isakeyword{infixl}\ {\isadigit{4}}\ {\isachardoublequoteopen}{\isacharequal}{\isacharequal}{\isachardoublequoteclose}{\isacharparenright}%
-\endisatagquotett
-{\isafoldquotett}%
+\endisatagtt
+{\isafoldtt}%
 %
-\isadelimquotett
+\isadelimtt
 %
-\endisadelimquotett
+\endisadelimtt
 %
 \begin{isamarkuptext}%
 \noindent A problem now occurs whenever a type which is an instance
@@ -553,20 +553,20 @@
 %
 \endisadelimquote
 %
-\isadelimquotett
+\isadelimtt
 \ %
-\endisadelimquotett
+\endisadelimtt
 %
-\isatagquotett
+\isatagtt
 \isacommand{code{\isacharunderscore}type}\isamarkupfalse%
 \ bar\isanewline
 \ \ {\isacharparenleft}Haskell\ {\isachardoublequoteopen}Integer{\isachardoublequoteclose}{\isacharparenright}%
-\endisatagquotett
-{\isafoldquotett}%
+\endisatagtt
+{\isafoldtt}%
 %
-\isadelimquotett
+\isadelimtt
 %
-\endisadelimquotett
+\endisadelimtt
 %
 \begin{isamarkuptext}%
 \noindent The code generator would produce an additional instance,
@@ -575,20 +575,20 @@
 \end{isamarkuptext}%
 \isamarkuptrue%
 %
-\isadelimquotett
+\isadelimtt
 %
-\endisadelimquotett
+\endisadelimtt
 %
-\isatagquotett
+\isatagtt
 \isacommand{code{\isacharunderscore}instance}\isamarkupfalse%
 \ bar\ {\isacharcolon}{\isacharcolon}\ equal\isanewline
 \ \ {\isacharparenleft}Haskell\ {\isacharminus}{\isacharparenright}%
-\endisatagquotett
-{\isafoldquotett}%
+\endisatagtt
+{\isafoldtt}%
 %
-\isadelimquotett
+\isadelimtt
 %
-\endisadelimquotett
+\endisadelimtt
 %
 \isamarkupsubsection{Enhancing the target language context \label{sec:include}%
 }
@@ -600,23 +600,23 @@
 \end{isamarkuptext}%
 \isamarkuptrue%
 %
-\isadelimquotett
+\isadelimtt
 %
-\endisadelimquotett
+\endisadelimtt
 %
-\isatagquotett
+\isatagtt
 \isacommand{code{\isacharunderscore}include}\isamarkupfalse%
 \ Haskell\ {\isachardoublequoteopen}Errno{\isachardoublequoteclose}\isanewline
 {\isacharverbatimopen}errno\ i\ {\isacharequal}\ error\ {\isacharparenleft}{\isachardoublequote}Error\ number{\isacharcolon}\ {\isachardoublequote}\ {\isacharplus}{\isacharplus}\ show\ i{\isacharparenright}{\isacharverbatimclose}\isanewline
 \isanewline
 \isacommand{code{\isacharunderscore}reserved}\isamarkupfalse%
 \ Haskell\ Errno%
-\endisatagquotett
-{\isafoldquotett}%
+\endisatagtt
+{\isafoldtt}%
 %
-\isadelimquotett
+\isadelimtt
 %
-\endisadelimquotett
+\endisadelimtt
 %
 \begin{isamarkuptext}%
 \noindent Such named \isa{include}s are then prepended to every
diff -r 6542245db5c2 -r d3f46f1ca1f1 doc-src/Codegen/Thy/document/Evaluation.tex
--- a/doc-src/Codegen/Thy/document/Evaluation.tex	Sat Sep 25 10:32:14 2010 +0200
+++ b/doc-src/Codegen/Thy/document/Evaluation.tex	Mon Sep 27 08:47:23 2010 +0200
@@ -269,20 +269,7 @@
 %
 \isatagquote
 \isacommand{datatype}\isamarkupfalse%
-\ form\ {\isacharequal}\ T\ {\isacharbar}\ F\ {\isacharbar}\ And\ form\ form\ {\isacharbar}\ Or\ form\ form\ %
-\endisatagquote
-{\isafoldquote}%
-%
-\isadelimquote
-%
-\endisadelimquote
-%
-\isadelimquotett
-\ %
-\endisadelimquotett
-%
-\isatagquotett
-\isacommand{ML}\isamarkupfalse%
+\ form\ {\isacharequal}\ T\ {\isacharbar}\ F\ {\isacharbar}\ And\ form\ form\ {\isacharbar}\ Or\ form\ form\ \ \isacommand{ML}\isamarkupfalse%
 \ {\isacharverbatimopen}\isanewline
 \ \ fun\ eval{\isacharunderscore}form\ %
 \isaantiq
@@ -307,12 +294,12 @@
 \ {\isacharparenleft}p{\isacharcomma}\ q{\isacharparenright}{\isacharparenright}\ {\isacharequal}\isanewline
 \ \ \ \ \ \ \ \ eval{\isacharunderscore}form\ p\ orelse\ eval{\isacharunderscore}form\ q{\isacharsemicolon}\isanewline
 {\isacharverbatimclose}%
-\endisatagquotett
-{\isafoldquotett}%
+\endisatagquote
+{\isafoldquote}%
 %
-\isadelimquotett
+\isadelimquote
 %
-\endisadelimquotett
+\endisadelimquote
 %
 \begin{isamarkuptext}%
 \noindent \isa{code} takes as argument the name of a constant;
diff -r 6542245db5c2 -r d3f46f1ca1f1 doc-src/Codegen/style.sty
--- a/doc-src/Codegen/style.sty	Sat Sep 25 10:32:14 2010 +0200
+++ b/doc-src/Codegen/style.sty	Mon Sep 27 08:47:23 2010 +0200
@@ -37,9 +37,8 @@
 \renewcommand{\isatagtypewriter}{\begin{typewriter}}
 \renewcommand{\endisatagtypewriter}{\end{typewriter}}
 
-\isakeeptag{quotett}
-\renewcommand{\isatagquotett}{\begin{quote}\isabellestyle{tt}\isastyle}
-\renewcommand{\endisatagquotett}{\end{quote}}
+\isakeeptag{tt}
+\renewcommand{\isatagtt}{\isabellestyle{tt}\isastyle}
 
 %% a trick
 \newcommand{\isasymSML}{SML}