# HG changeset patch
# User haftmann
# Date 1236082853 -3600
# Node ID 853abb4853cc8179bef5281480483ebe5c1e94ef
# Parent  2f4684e2ea954d317d5c0f300ad35c6d38ae6826
tuned manuals

diff -r 2f4684e2ea95 -r 853abb4853cc doc-src/Classes/Thy/Classes.thy
--- a/doc-src/Classes/Thy/Classes.thy	Tue Mar 03 11:00:51 2009 +0100
+++ b/doc-src/Classes/Thy/Classes.thy	Tue Mar 03 13:20:53 2009 +0100
@@ -2,8 +2,6 @@
 imports Main Setup
 begin
 
-chapter {* Haskell-style classes with Isabelle/Isar *}
-
 section {* Introduction *}
 
 text {*
@@ -17,10 +15,11 @@
   types for @{text "\<alpha>"}, which is achieved by splitting introduction
   of the @{text eq} function from its overloaded definitions by means
   of @{text class} and @{text instance} declarations:
+  \footnote{syntax here is a kind of isabellized Haskell}
 
   \begin{quote}
 
-  \noindent@{text "class eq where"}\footnote{syntax here is a kind of isabellized Haskell} \\
+  \noindent@{text "class eq where"} \\
   \hspace*{2ex}@{text "eq \<Colon> \<alpha> \<Rightarrow> \<alpha> \<Rightarrow> bool"}
 
   \medskip\noindent@{text "instance nat \<Colon> eq where"} \\
@@ -355,8 +354,8 @@
 
 text {*
   \noindent essentially introduces the locale
-*} setup %invisible {* Sign.add_path "foo" *}
-
+*} (*<*)setup %invisible {* Sign.add_path "foo" *}
+(*>*)
 locale %quote idem =
   fixes f :: "\<alpha> \<Rightarrow> \<alpha>"
   assumes idem: "f (f x) = f x"
@@ -368,10 +367,10 @@
 text {*
   \noindent The connection to the type system is done by means
   of a primitive axclass
-*} setup %invisible {* Sign.add_path "foo" *}
-
+*} (*<*)setup %invisible {* Sign.add_path "foo" *}
+(*>*)
 axclass %quote idem < type
-  idem: "f (f x) = f x" setup %invisible {* Sign.parent_path *}
+  idem: "f (f x) = f x" (*<*)setup %invisible {* Sign.parent_path *}(*>*)
 
 text {* \noindent together with a corresponding interpretation: *}
 
@@ -383,8 +382,8 @@
   \noindent This gives you at hand the full power of the Isabelle module system;
   conclusions in locale @{text idem} are implicitly propagated
   to class @{text idem}.
-*} setup %invisible {* Sign.parent_path *}
-
+*} (*<*)setup %invisible {* Sign.parent_path *}
+(*>*)
 subsection {* Abstract reasoning *}
 
 text {*
@@ -505,7 +504,7 @@
 qed
 
 text {*
-  \noindent The logical proof is carried out on the locale level.
+  The logical proof is carried out on the locale level.
   Afterwards it is propagated
   to the type system, making @{text group} an instance of
   @{text monoid} by adding an additional edge
@@ -541,7 +540,7 @@
      \label{fig:subclass}
    \end{center}
   \end{figure}
-7
+
   For illustration, a derived definition
   in @{text group} which uses @{text pow_nat}:
 *}
diff -r 2f4684e2ea95 -r 853abb4853cc doc-src/Classes/Thy/Setup.thy
--- a/doc-src/Classes/Thy/Setup.thy	Tue Mar 03 11:00:51 2009 +0100
+++ b/doc-src/Classes/Thy/Setup.thy	Tue Mar 03 13:20:53 2009 +0100
@@ -1,8 +1,8 @@
 theory Setup
 imports Main Code_Integer
 uses
-  "../../../antiquote_setup"
-  "../../../more_antiquote"
+  "../../antiquote_setup"
+  "../../more_antiquote"
 begin
 
 ML {* Code_Target.code_width := 74 *}
diff -r 2f4684e2ea95 -r 853abb4853cc doc-src/Classes/Thy/document/Classes.tex
--- a/doc-src/Classes/Thy/document/Classes.tex	Tue Mar 03 11:00:51 2009 +0100
+++ b/doc-src/Classes/Thy/document/Classes.tex	Tue Mar 03 13:20:53 2009 +0100
@@ -18,10 +18,6 @@
 %
 \endisadelimtheory
 %
-\isamarkupchapter{Haskell-style classes with Isabelle/Isar%
-}
-\isamarkuptrue%
-%
 \isamarkupsection{Introduction%
 }
 \isamarkuptrue%
@@ -37,10 +33,11 @@
   types for \isa{{\isasymalpha}}, which is achieved by splitting introduction
   of the \isa{eq} function from its overloaded definitions by means
   of \isa{class} and \isa{instance} declarations:
+  \footnote{syntax here is a kind of isabellized Haskell}
 
   \begin{quote}
 
-  \noindent\isa{class\ eq\ where}\footnote{syntax here is a kind of isabellized Haskell} \\
+  \noindent\isa{class\ eq\ where} \\
   \hspace*{2ex}\isa{eq\ {\isasymColon}\ {\isasymalpha}\ {\isasymRightarrow}\ {\isasymalpha}\ {\isasymRightarrow}\ bool}
 
   \medskip\noindent\isa{instance\ nat\ {\isasymColon}\ eq\ where} \\
@@ -597,24 +594,21 @@
 \noindent essentially introduces the locale%
 \end{isamarkuptext}%
 \isamarkuptrue%
-%
+\ %
 \isadeliminvisible
-\ %
+%
 \endisadeliminvisible
 %
 \isataginvisible
-\isacommand{setup}\isamarkupfalse%
-\ {\isacharverbatimopen}\ Sign{\isachardot}add{\isacharunderscore}path\ {\isachardoublequote}foo{\isachardoublequote}\ {\isacharverbatimclose}%
+%
 \endisataginvisible
 {\isafoldinvisible}%
 %
 \isadeliminvisible
 %
 \endisadeliminvisible
-\isanewline
 %
 \isadelimquote
-\isanewline
 %
 \endisadelimquote
 %
@@ -654,31 +648,28 @@
   of a primitive axclass%
 \end{isamarkuptext}%
 \isamarkuptrue%
-%
+\ %
 \isadeliminvisible
-\ %
+%
 \endisadeliminvisible
 %
 \isataginvisible
-\isacommand{setup}\isamarkupfalse%
-\ {\isacharverbatimopen}\ Sign{\isachardot}add{\isacharunderscore}path\ {\isachardoublequote}foo{\isachardoublequote}\ {\isacharverbatimclose}%
+%
 \endisataginvisible
 {\isafoldinvisible}%
 %
 \isadeliminvisible
 %
 \endisadeliminvisible
-\isanewline
 %
 \isadelimquote
-\isanewline
 %
 \endisadelimquote
 %
 \isatagquote
 \isacommand{axclass}\isamarkupfalse%
 \ idem\ {\isacharless}\ type\isanewline
-\ \ idem{\isacharcolon}\ {\isachardoublequoteopen}f\ {\isacharparenleft}f\ x{\isacharparenright}\ {\isacharequal}\ f\ x{\isachardoublequoteclose}%
+\ \ idem{\isacharcolon}\ {\isachardoublequoteopen}f\ {\isacharparenleft}f\ x{\isacharparenright}\ {\isacharequal}\ f\ x{\isachardoublequoteclose}\ %
 \endisatagquote
 {\isafoldquote}%
 %
@@ -687,12 +678,11 @@
 \endisadelimquote
 %
 \isadeliminvisible
-\ %
+%
 \endisadeliminvisible
 %
 \isataginvisible
-\isacommand{setup}\isamarkupfalse%
-\ {\isacharverbatimopen}\ Sign{\isachardot}parent{\isacharunderscore}path\ {\isacharverbatimclose}%
+%
 \endisataginvisible
 {\isafoldinvisible}%
 %
@@ -729,14 +719,13 @@
   to class \isa{idem}.%
 \end{isamarkuptext}%
 \isamarkuptrue%
-%
+\ %
 \isadeliminvisible
-\ %
+%
 \endisadeliminvisible
 %
 \isataginvisible
-\isacommand{setup}\isamarkupfalse%
-\ {\isacharverbatimopen}\ Sign{\isachardot}parent{\isacharunderscore}path\ {\isacharverbatimclose}%
+%
 \endisataginvisible
 {\isafoldinvisible}%
 %
@@ -978,7 +967,7 @@
 \endisadelimquote
 %
 \begin{isamarkuptext}%
-\noindent The logical proof is carried out on the locale level.
+The logical proof is carried out on the locale level.
   Afterwards it is propagated
   to the type system, making \isa{group} an instance of
   \isa{monoid} by adding an additional edge
@@ -1010,11 +999,11 @@
      \end{picture}
      \caption{Subclass relationship of monoids and groups:
         before and after establishing the relationship
-        \isa{group\ {\isasymsubseteq}\ monoid};  transitive edges left out.}
+        \isa{group\ {\isasymsubseteq}\ monoid};  transitive edges are left out.}
      \label{fig:subclass}
    \end{center}
   \end{figure}
-7
+
   For illustration, a derived definition
   in \isa{group} which uses \isa{pow{\isacharunderscore}nat}:%
 \end{isamarkuptext}%
diff -r 2f4684e2ea95 -r 853abb4853cc doc-src/Classes/classes.tex
--- a/doc-src/Classes/classes.tex	Tue Mar 03 11:00:51 2009 +0100
+++ b/doc-src/Classes/classes.tex	Tue Mar 03 13:20:53 2009 +0100
@@ -1,5 +1,5 @@
 
-\documentclass[12pt,a4paper,fleqn]{report}
+\documentclass[12pt,a4paper,fleqn]{article}
 \usepackage{latexsym,graphicx}
 \usepackage[refpage]{nomencl}
 \usepackage{../iman,../extra,../isar,../proof}
@@ -21,7 +21,7 @@
 \maketitle
 
 \begin{abstract}
-  This tutorial introduces the look-and-feel of Isar type classes
+  \noindent This tutorial introduces the look-and-feel of Isar type classes
   to the end-user; Isar type classes are a convenient mechanism
   for organizing specifications, overcoming some drawbacks
   of raw axiomatic type classes. Essentially, they combine
diff -r 2f4684e2ea95 -r 853abb4853cc doc-src/Classes/style.sty
--- a/doc-src/Classes/style.sty	Tue Mar 03 11:00:51 2009 +0100
+++ b/doc-src/Classes/style.sty	Tue Mar 03 13:20:53 2009 +0100
@@ -3,6 +3,9 @@
 \newcommand{\tocentry}[1]{\cleardoublepage\phantomsection\addcontentsline{toc}{chapter}{#1}
 \@mkboth{\MakeUppercase{#1}}{\MakeUppercase{#1}}}
 
+%% paragraphs
+\setlength{\parindent}{1em}
+
 %% references
 \newcommand{\secref}[1]{\S\ref{#1}}
 \newcommand{\figref}[1]{figure~\ref{#1}}
@@ -17,23 +20,25 @@
 %% verbatim text
 \newcommand{\isatypewriter}{\fontsize{9pt}{0pt}\tt\renewcommand{\baselinestretch}{1}\setlength{\baselineskip}{9pt}}
 
-%% quoted segments
-\makeatletter
+%% quote environment
 \isakeeptag{quote}
-\newenvironment{quotesegment}{\begin{quote}\isa@parindent\parindent\parindent0pt\isa@parskip\parskip\parskip0pt}{\end{quote}}
-\renewcommand{\isatagquote}{\begin{quotesegment}}
-\renewcommand{\endisatagquote}{\end{quotesegment}}
-\makeatother
+\renewenvironment{quote}
+  {\list{}{\leftmargin2em\rightmargin0pt}\parindent0pt\parskip0pt\item\relax}
+  {\endlist}
+\renewcommand{\isatagquote}{\begin{quote}}
+\renewcommand{\endisatagquote}{\end{quote}}
+\newcommand{\quotebreak}{\\[1.2ex]}
 
 %% presentation
 \setcounter{secnumdepth}{2} \setcounter{tocdepth}{2}
 
-\pagestyle{headings}
+%% character detail
+\renewcommand{\isadigit}[1]{\isamath{#1}}
 \binperiod
 \underscoreoff
 
-\renewcommand{\isadigit}[1]{\isamath{#1}}
-
+%% format
+\pagestyle{headings}
 \isabellestyle{it}
 
 
diff -r 2f4684e2ea95 -r 853abb4853cc doc-src/Codegen/Thy/Adaption.thy
--- a/doc-src/Codegen/Thy/Adaption.thy	Tue Mar 03 11:00:51 2009 +0100
+++ b/doc-src/Codegen/Thy/Adaption.thy	Tue Mar 03 13:20:53 2009 +0100
@@ -323,7 +323,6 @@
 instance %quote by default (simp add: eq_bar_def)
 
 end %quote
-
 code_type %quotett bar
   (Haskell "Integer")
 
diff -r 2f4684e2ea95 -r 853abb4853cc doc-src/Codegen/Thy/Codegen.thy
--- a/doc-src/Codegen/Thy/Codegen.thy	Tue Mar 03 11:00:51 2009 +0100
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,2 +0,0 @@
-
-end
diff -r 2f4684e2ea95 -r 853abb4853cc doc-src/Codegen/Thy/Further.thy
--- a/doc-src/Codegen/Thy/Further.thy	Tue Mar 03 11:00:51 2009 +0100
+++ b/doc-src/Codegen/Thy/Further.thy	Tue Mar 03 13:20:53 2009 +0100
@@ -79,8 +79,7 @@
 *}
 
 datatype %quote form = T | F | And form form | Or form form
-
-ML %quote {*
+ML %quotett {*
   fun eval_form @{code T} = true
     | eval_form @{code F} = false
     | eval_form (@{code And} (p, q)) =
diff -r 2f4684e2ea95 -r 853abb4853cc doc-src/Codegen/Thy/Introduction.thy
--- a/doc-src/Codegen/Thy/Introduction.thy	Tue Mar 03 11:00:51 2009 +0100
+++ b/doc-src/Codegen/Thy/Introduction.thy	Tue Mar 03 13:20:53 2009 +0100
@@ -2,8 +2,6 @@
 imports Setup
 begin
 
-chapter {* Code generation from @{text "Isabelle/HOL"} theories *}
-
 section {* Introduction and Overview *}
 
 text {*
diff -r 2f4684e2ea95 -r 853abb4853cc doc-src/Codegen/Thy/Program.thy
--- a/doc-src/Codegen/Thy/Program.thy	Tue Mar 03 11:00:51 2009 +0100
+++ b/doc-src/Codegen/Thy/Program.thy	Tue Mar 03 13:20:53 2009 +0100
@@ -287,16 +287,9 @@
   @{text case} combinator on queues:
 *}
 
-definition %quote
-  aqueue_case_def: "aqueue_case = queue_case"
-
-lemma %quote aqueue_case [code, code inline]:
-  "queue_case = aqueue_case"
-  unfolding aqueue_case_def ..
-
-lemma %quote case_AQueue [code]:
-  "aqueue_case f (AQueue xs ys) = f (ys @ rev xs)"
-  unfolding aqueue_case_def AQueue_def by simp
+lemma %quote queue_case_AQueue [code]:
+  "queue_case f (AQueue xs ys) = f (ys @ rev xs)"
+  unfolding AQueue_def by simp
 
 text {*
   \noindent The resulting code looks as expected:
@@ -313,8 +306,7 @@
   \begin{itemize}
 
     \item When changing the constructor set for datatypes, take care
-      to provide an alternative for the @{text case} combinator
-      (e.g.~by replacing it using the preprocessor).
+      to provide alternative equations for the @{text case} combinator.
 
     \item Values in the target language need not to be normalised --
       different values in the target language may represent the same
diff -r 2f4684e2ea95 -r 853abb4853cc doc-src/Codegen/Thy/Setup.thy
--- a/doc-src/Codegen/Thy/Setup.thy	Tue Mar 03 11:00:51 2009 +0100
+++ b/doc-src/Codegen/Thy/Setup.thy	Tue Mar 03 13:20:53 2009 +0100
@@ -1,12 +1,15 @@
 theory Setup
 imports Complex_Main
-uses "../../../antiquote_setup.ML" "../../../more_antiquote.ML"
+uses
+  "../../antiquote_setup.ML"
+  "../../more_antiquote.ML"
 begin
 
 ML {* no_document use_thys
   ["Efficient_Nat", "Code_Char_chr", "Product_ord", "~~/src/HOL/Imperative_HOL/Imperative_HOL",
    "~~/src/HOL/Decision_Procs/Ferrack"] *}
 
-ML_val {* Code_Target.code_width := 74 *}
+ML_command {* Code_Target.code_width := 74 *}
+ML_command {* reset unique_names *}
 
 end
diff -r 2f4684e2ea95 -r 853abb4853cc doc-src/Codegen/Thy/document/Adaption.tex
--- a/doc-src/Codegen/Thy/document/Adaption.tex	Tue Mar 03 11:00:51 2009 +0100
+++ b/doc-src/Codegen/Thy/document/Adaption.tex	Tue Mar 03 13:20:53 2009 +0100
@@ -583,7 +583,6 @@
 \isanewline
 %
 \isadelimquotett
-\isanewline
 %
 \endisadelimquotett
 %
diff -r 2f4684e2ea95 -r 853abb4853cc doc-src/Codegen/Thy/document/Further.tex
--- a/doc-src/Codegen/Thy/document/Further.tex	Tue Mar 03 11:00:51 2009 +0100
+++ b/doc-src/Codegen/Thy/document/Further.tex	Tue Mar 03 13:20:53 2009 +0100
@@ -154,8 +154,20 @@
 %
 \isatagquote
 \isacommand{datatype}\isamarkupfalse%
-\ form\ {\isacharequal}\ T\ {\isacharbar}\ F\ {\isacharbar}\ And\ form\ form\ {\isacharbar}\ Or\ form\ form\isanewline
+\ form\ {\isacharequal}\ T\ {\isacharbar}\ F\ {\isacharbar}\ And\ form\ form\ {\isacharbar}\ Or\ form\ form%
+\endisatagquote
+{\isafoldquote}%
+%
+\isadelimquote
+%
+\endisadelimquote
 \isanewline
+%
+\isadelimquotett
+%
+\endisadelimquotett
+%
+\isatagquotett
 \isacommand{ML}\isamarkupfalse%
 \ {\isacharverbatimopen}\isanewline
 \ \ fun\ eval{\isacharunderscore}form\ %
@@ -181,12 +193,12 @@
 \ {\isacharparenleft}p{\isacharcomma}\ q{\isacharparenright}{\isacharparenright}\ {\isacharequal}\isanewline
 \ \ \ \ \ \ \ \ eval{\isacharunderscore}form\ p\ orelse\ eval{\isacharunderscore}form\ q{\isacharsemicolon}\isanewline
 {\isacharverbatimclose}%
-\endisatagquote
-{\isafoldquote}%
+\endisatagquotett
+{\isafoldquotett}%
 %
-\isadelimquote
+\isadelimquotett
 %
-\endisadelimquote
+\endisadelimquotett
 %
 \begin{isamarkuptext}%
 \noindent \isa{code} takes as argument the name of a constant;  after the
diff -r 2f4684e2ea95 -r 853abb4853cc doc-src/Codegen/Thy/document/Introduction.tex
--- a/doc-src/Codegen/Thy/document/Introduction.tex	Tue Mar 03 11:00:51 2009 +0100
+++ b/doc-src/Codegen/Thy/document/Introduction.tex	Tue Mar 03 13:20:53 2009 +0100
@@ -18,10 +18,6 @@
 %
 \endisadelimtheory
 %
-\isamarkupchapter{Code generation from \isa{Isabelle{\isacharslash}HOL} theories%
-}
-\isamarkuptrue%
-%
 \isamarkupsection{Introduction and Overview%
 }
 \isamarkuptrue%
diff -r 2f4684e2ea95 -r 853abb4853cc doc-src/Codegen/Thy/document/Program.tex
--- a/doc-src/Codegen/Thy/document/Program.tex	Tue Mar 03 11:00:51 2009 +0100
+++ b/doc-src/Codegen/Thy/document/Program.tex	Tue Mar 03 13:20:53 2009 +0100
@@ -573,7 +573,7 @@
 \endisadelimquote
 %
 \begin{isamarkuptext}%
-\noindent Here we define a \qt{constructor} \isa{Program{\isachardot}AQueue} which
+\noindent Here we define a \qt{constructor} \isa{AQueue} which
   is defined in terms of \isa{Queue} and interprets its arguments
   according to what the \emph{content} of an amortised queue is supposed
   to be.  Equipped with this, we are able to prove the following equations
@@ -628,22 +628,11 @@
 \endisadelimquote
 %
 \isatagquote
-\isacommand{definition}\isamarkupfalse%
-\isanewline
-\ \ aqueue{\isacharunderscore}case{\isacharunderscore}def{\isacharcolon}\ {\isachardoublequoteopen}aqueue{\isacharunderscore}case\ {\isacharequal}\ queue{\isacharunderscore}case{\isachardoublequoteclose}\isanewline
-\isanewline
 \isacommand{lemma}\isamarkupfalse%
-\ aqueue{\isacharunderscore}case\ {\isacharbrackleft}code{\isacharcomma}\ code\ inline{\isacharbrackright}{\isacharcolon}\isanewline
-\ \ {\isachardoublequoteopen}queue{\isacharunderscore}case\ {\isacharequal}\ aqueue{\isacharunderscore}case{\isachardoublequoteclose}\isanewline
+\ queue{\isacharunderscore}case{\isacharunderscore}AQueue\ {\isacharbrackleft}code{\isacharbrackright}{\isacharcolon}\isanewline
+\ \ {\isachardoublequoteopen}queue{\isacharunderscore}case\ f\ {\isacharparenleft}AQueue\ xs\ ys{\isacharparenright}\ {\isacharequal}\ f\ {\isacharparenleft}ys\ {\isacharat}\ rev\ xs{\isacharparenright}{\isachardoublequoteclose}\isanewline
 \ \ \isacommand{unfolding}\isamarkupfalse%
-\ aqueue{\isacharunderscore}case{\isacharunderscore}def\ \isacommand{{\isachardot}{\isachardot}}\isamarkupfalse%
-\isanewline
-\isanewline
-\isacommand{lemma}\isamarkupfalse%
-\ case{\isacharunderscore}AQueue\ {\isacharbrackleft}code{\isacharbrackright}{\isacharcolon}\isanewline
-\ \ {\isachardoublequoteopen}aqueue{\isacharunderscore}case\ f\ {\isacharparenleft}AQueue\ xs\ ys{\isacharparenright}\ {\isacharequal}\ f\ {\isacharparenleft}ys\ {\isacharat}\ rev\ xs{\isacharparenright}{\isachardoublequoteclose}\isanewline
-\ \ \isacommand{unfolding}\isamarkupfalse%
-\ aqueue{\isacharunderscore}case{\isacharunderscore}def\ AQueue{\isacharunderscore}def\ \isacommand{by}\isamarkupfalse%
+\ AQueue{\isacharunderscore}def\ \isacommand{by}\isamarkupfalse%
 \ simp%
 \endisatagquote
 {\isafoldquote}%
@@ -708,8 +697,7 @@
   \begin{itemize}
 
     \item When changing the constructor set for datatypes, take care
-      to provide an alternative for the \isa{case} combinator
-      (e.g.~by replacing it using the preprocessor).
+      to provide alternative equations for the \isa{case} combinator.
 
     \item Values in the target language need not to be normalised --
       different values in the target language may represent the same
@@ -1098,7 +1086,7 @@
 %
 \begin{isamarkuptext}%
 \noindent In the corresponding code, there is no equation
-  for the pattern \isa{Program{\isachardot}AQueue\ {\isacharbrackleft}{\isacharbrackright}\ {\isacharbrackleft}{\isacharbrackright}}:%
+  for the pattern \isa{AQueue\ {\isacharbrackleft}{\isacharbrackright}\ {\isacharbrackleft}{\isacharbrackright}}:%
 \end{isamarkuptext}%
 \isamarkuptrue%
 %
diff -r 2f4684e2ea95 -r 853abb4853cc doc-src/Codegen/codegen.tex
--- a/doc-src/Codegen/codegen.tex	Tue Mar 03 11:00:51 2009 +0100
+++ b/doc-src/Codegen/codegen.tex	Tue Mar 03 13:20:53 2009 +0100
@@ -1,5 +1,5 @@
 
-\documentclass[12pt,a4paper,fleqn]{report}
+\documentclass[12pt,a4paper,fleqn]{article}
 \usepackage{latexsym,graphicx}
 \usepackage[refpage]{nomencl}
 \usepackage{../iman,../extra,../isar,../proof}
@@ -23,7 +23,7 @@
 \maketitle
 
 \begin{abstract}
-  This tutorial gives an introduction to a generic code generator framework in Isabelle
+  \noindent This tutorial gives an introduction to a generic code generator framework in Isabelle
   for generating executable code in functional programming languages from logical
   specifications in Isabelle/HOL.
 \end{abstract}
diff -r 2f4684e2ea95 -r 853abb4853cc doc-src/Codegen/style.sty
--- a/doc-src/Codegen/style.sty	Tue Mar 03 11:00:51 2009 +0100
+++ b/doc-src/Codegen/style.sty	Tue Mar 03 13:20:53 2009 +0100
@@ -3,6 +3,9 @@
 \newcommand{\tocentry}[1]{\cleardoublepage\phantomsection\addcontentsline{toc}{chapter}{#1}
 \@mkboth{\MakeUppercase{#1}}{\MakeUppercase{#1}}}
 
+%% paragraphs
+\setlength{\parindent}{1em}
+
 %% references
 \newcommand{\secref}[1]{\S\ref{#1}}
 
@@ -16,17 +19,18 @@
 %% verbatim text
 \newcommand{\isatypewriter}{\fontsize{9pt}{0pt}\tt\renewcommand{\baselinestretch}{1}\setlength{\baselineskip}{9pt}}
 
-%% quoted segments
-\makeatletter
+%% quote environment
 \isakeeptag{quote}
-\newenvironment{quotesegment}{\begin{quote}\isa@parindent\parindent\parindent0pt\isa@parskip\parskip\parskip0pt}{\end{quote}}
-\renewcommand{\isatagquote}{\begin{quotesegment}}
-\renewcommand{\endisatagquote}{\end{quotesegment}}
-\makeatother
+\renewenvironment{quote}
+  {\list{}{\leftmargin2em\rightmargin0pt}\parindent0pt\parskip0pt\item\relax}
+  {\endlist}
+\renewcommand{\isatagquote}{\begin{quote}}
+\renewcommand{\endisatagquote}{\end{quote}}
+\newcommand{\quotebreak}{\\[1.2ex]}
 
 \isakeeptag{quotett}
-\renewcommand{\isatagquotett}{\begin{quotesegment}\isabellestyle{tt}\isastyle}
-\renewcommand{\endisatagquotett}{\end{quotesegment}\isabellestyle{it}\isastyle}
+\renewcommand{\isatagquotett}{\begin{quote}\isabellestyle{tt}\isastyle}
+\renewcommand{\endisatagquotett}{\end{quote}\isabellestyle{it}\isastyle}
 
 %% a trick
 \newcommand{\isasymSML}{SML}
@@ -34,11 +38,14 @@
 %% presentation
 \setcounter{secnumdepth}{2} \setcounter{tocdepth}{2}
 
-\pagestyle{headings}
+%% character detail
+\renewcommand{\isadigit}[1]{\isamath{#1}}
 \binperiod
 \underscoreoff
 
-\renewcommand{\isadigit}[1]{\isamath{#1}}
+%% format
+\pagestyle{headings}
+\isabellestyle{it}
 
 %% ml reference
 \newenvironment{mldecls}{\par\noindent\begingroup\footnotesize\def\isanewline{\\}\begin{tabular}{l}}{\end{tabular}\smallskip\endgroup}