# HG changeset patch
# User haftmann
# Date 1223646765 -7200
# Node ID 519b171189266660ad487ec786b79656b655d7f9
# Parent  1358b1ddd915ccee4401bbfd084be37b3aa0e5de
tuned

diff -r 1358b1ddd915 -r 519b17118926 doc-src/IsarAdvanced/Classes/Thy/Classes.thy
--- a/doc-src/IsarAdvanced/Classes/Thy/Classes.thy	Fri Oct 10 15:23:33 2008 +0200
+++ b/doc-src/IsarAdvanced/Classes/Thy/Classes.thy	Fri Oct 10 15:52:45 2008 +0200
@@ -1,41 +1,7 @@
-(* $Id$ *)
-
-(*<*)
 theory Classes
-imports Main Code_Integer
-uses "../../../more_antiquote"
+imports Main Setup
 begin
 
-ML {*
-Code_Target.code_width := 74;
-*}
-
-syntax
-  "_alpha" :: "type"  ("\<alpha>")
-  "_alpha_ofsort" :: "sort \<Rightarrow> type"  ("\<alpha>()\<Colon>_" [0] 1000)
-  "_beta" :: "type"  ("\<beta>")
-  "_beta_ofsort" :: "sort \<Rightarrow> type"  ("\<beta>()\<Colon>_" [0] 1000)
-
-parse_ast_translation {*
-  let
-    fun alpha_ast_tr [] = Syntax.Variable "'a"
-      | alpha_ast_tr asts = raise Syntax.AST ("alpha_ast_tr", asts);
-    fun alpha_ofsort_ast_tr [ast] =
-      Syntax.Appl [Syntax.Constant "_ofsort", Syntax.Variable "'a", ast]
-      | alpha_ofsort_ast_tr asts = raise Syntax.AST ("alpha_ast_tr", asts);
-    fun beta_ast_tr [] = Syntax.Variable "'b"
-      | beta_ast_tr asts = raise Syntax.AST ("beta_ast_tr", asts);
-    fun beta_ofsort_ast_tr [ast] =
-      Syntax.Appl [Syntax.Constant "_ofsort", Syntax.Variable "'b", ast]
-      | beta_ofsort_ast_tr asts = raise Syntax.AST ("beta_ast_tr", asts);
-  in [
-    ("_alpha", alpha_ast_tr), ("_alpha_ofsort", alpha_ofsort_ast_tr),
-    ("_beta", beta_ast_tr), ("_beta_ofsort", beta_ofsort_ast_tr)
-  ] end
-*}
-(*>*)
-
-
 chapter {* Haskell-style classes with Isabelle/Isar *}
 
 section {* Introduction *}
@@ -52,23 +18,27 @@
   of the @{text eq} function from its overloaded definitions by means
   of @{text class} and @{text instance} declarations:
 
-  \medskip\noindent\hspace*{2ex}@{text "class eq where"}\footnote{syntax here is a kind of isabellized Haskell} \\
-  \hspace*{4ex}@{text "eq \<Colon> \<alpha> \<Rightarrow> \<alpha> \<Rightarrow> bool"}
+  \begin{quote}
+
+  \noindent@{text "class eq where"}\footnote{syntax here is a kind of isabellized Haskell} \\
+  \hspace*{2ex}@{text "eq \<Colon> \<alpha> \<Rightarrow> \<alpha> \<Rightarrow> bool"}
 
-  \medskip\noindent\hspace*{2ex}@{text "instance nat \<Colon> eq where"} \\
-  \hspace*{4ex}@{text "eq 0 0 = True"} \\
-  \hspace*{4ex}@{text "eq 0 _ = False"} \\
-  \hspace*{4ex}@{text "eq _ 0 = False"} \\
-  \hspace*{4ex}@{text "eq (Suc n) (Suc m) = eq n m"}
+  \medskip\noindent@{text "instance nat \<Colon> eq where"} \\
+  \hspace*{2ex}@{text "eq 0 0 = True"} \\
+  \hspace*{2ex}@{text "eq 0 _ = False"} \\
+  \hspace*{2ex}@{text "eq _ 0 = False"} \\
+  \hspace*{2ex}@{text "eq (Suc n) (Suc m) = eq n m"}
 
-  \medskip\noindent\hspace*{2ex}@{text "instance (\<alpha>\<Colon>eq, \<beta>\<Colon>eq) pair \<Colon> eq where"} \\
-  \hspace*{4ex}@{text "eq (x1, y1) (x2, y2) = eq x1 x2 \<and> eq y1 y2"}
+  \medskip\noindent\@{text "instance (\<alpha>\<Colon>eq, \<beta>\<Colon>eq) pair \<Colon> eq where"} \\
+  \hspace*{2ex}@{text "eq (x1, y1) (x2, y2) = eq x1 x2 \<and> eq y1 y2"}
 
-  \medskip\noindent\hspace*{2ex}@{text "class ord extends eq where"} \\
-  \hspace*{4ex}@{text "less_eq \<Colon> \<alpha> \<Rightarrow> \<alpha> \<Rightarrow> bool"} \\
-  \hspace*{4ex}@{text "less \<Colon> \<alpha> \<Rightarrow> \<alpha> \<Rightarrow> bool"}
+  \medskip\noindent@{text "class ord extends eq where"} \\
+  \hspace*{2ex}@{text "less_eq \<Colon> \<alpha> \<Rightarrow> \<alpha> \<Rightarrow> bool"} \\
+  \hspace*{2ex}@{text "less \<Colon> \<alpha> \<Rightarrow> \<alpha> \<Rightarrow> bool"}
 
-  \medskip\noindent Type variables are annotated with (finitely many) classes;
+  \end{quote}
+
+  \noindent Type variables are annotated with (finitely many) classes;
   these annotations are assertions that a particular polymorphic type
   provides definitions for overloaded functions.
 
@@ -85,14 +55,18 @@
   @{text "class eq"} is an equivalence relation obeying reflexivity,
   symmetry and transitivity:
 
-  \medskip\noindent\hspace*{2ex}@{text "class eq where"} \\
-  \hspace*{4ex}@{text "eq \<Colon> \<alpha> \<Rightarrow> \<alpha> \<Rightarrow> bool"} \\
-  \hspace*{2ex}@{text "satisfying"} \\
-  \hspace*{4ex}@{text "refl: eq x x"} \\
-  \hspace*{4ex}@{text "sym: eq x y \<longleftrightarrow> eq x y"} \\
-  \hspace*{4ex}@{text "trans: eq x y \<and> eq y z \<longrightarrow> eq x z"}
+  \begin{quote}
 
-  \medskip\noindent From a theoretic point of view, type classes are lightweight
+  \noindent@{text "class eq where"} \\
+  \hspace*{2ex}@{text "eq \<Colon> \<alpha> \<Rightarrow> \<alpha> \<Rightarrow> bool"} \\
+  @{text "satisfying"} \\
+  \hspace*{2ex}@{text "refl: eq x x"} \\
+  \hspace*{2ex}@{text "sym: eq x y \<longleftrightarrow> eq x y"} \\
+  \hspace*{2ex}@{text "trans: eq x y \<and> eq y z \<longrightarrow> eq x z"}
+
+  \end{quote}
+
+  \noindent From a theoretic point of view, type classes are lightweight
   modules; Haskell type classes may be emulated by
   SML functors \cite{classes_modules}. 
   Isabelle/Isar offers a discipline of type classes which brings
@@ -128,22 +102,23 @@
 
 text {*
   Depending on an arbitrary type @{text "\<alpha>"}, class @{text
-  "semigroup"} introduces a binary operator @{text "\<otimes>"} that is
+  "semigroup"} introduces a binary operator @{text "(\<otimes>)"} that is
   assumed to be associative:
 *}
 
-    class semigroup = type +
-      fixes mult :: "\<alpha> \<Rightarrow> \<alpha> \<Rightarrow> \<alpha>"    (infixl "\<otimes>" 70)
-      assumes assoc: "(x \<otimes> y) \<otimes> z = x \<otimes> (y \<otimes> z)"
+class %quote semigroup = type +
+  fixes mult :: "\<alpha> \<Rightarrow> \<alpha> \<Rightarrow> \<alpha>"    (infixl "\<otimes>" 70)
+  assumes assoc: "(x \<otimes> y) \<otimes> z = x \<otimes> (y \<otimes> z)"
 
 text {*
-  \noindent This @{text "\<CLASS>"} specification consists of two
-  parts: the \qn{operational} part names the class parameter (@{text
-  "\<FIXES>"}), the \qn{logical} part specifies properties on them
-  (@{text "\<ASSUMES>"}).  The local @{text "\<FIXES>"} and @{text
-  "\<ASSUMES>"} are lifted to the theory toplevel, yielding the global
+  \noindent This @{command class} specification consists of two
+  parts: the \qn{operational} part names the class parameter
+  (@{element "fixes"}), the \qn{logical} part specifies properties on them
+  (@{element "assumes"}).  The local @{element "fixes"} and
+  @{element "assumes"} are lifted to the theory toplevel,
+  yielding the global
   parameter @{term [source] "mult \<Colon> \<alpha>\<Colon>semigroup \<Rightarrow> \<alpha> \<Rightarrow> \<alpha>"} and the
-  global theorem @{text "semigroup.assoc:"}~@{prop [source] "\<And>x y
+  global theorem @{fact "semigroup.assoc:"}~@{prop [source] "\<And>x y
   z \<Colon> \<alpha>\<Colon>semigroup. (x \<otimes> y) \<otimes> z = x \<otimes> (y \<otimes> z)"}.
 *}
 
@@ -151,65 +126,66 @@
 subsection {* Class instantiation \label{sec:class_inst} *}
 
 text {*
-  The concrete type @{text "int"} is made a @{text "semigroup"}
+  The concrete type @{typ int} is made a @{class semigroup}
   instance by providing a suitable definition for the class parameter
-  @{text "mult"} and a proof for the specification of @{text "assoc"}.
-  This is accomplished by the @{text "\<INSTANTIATION>"} target:
+  @{text "(\<otimes>)"} and a proof for the specification of @{fact assoc}.
+  This is accomplished by the @{command instantiation} target:
 *}
 
-    instantiation int :: semigroup
-    begin
+instantiation %quote int :: semigroup
+begin
 
-    definition
-      mult_int_def: "i \<otimes> j = i + (j\<Colon>int)"
+definition %quote
+  mult_int_def: "i \<otimes> j = i + (j\<Colon>int)"
 
-    instance proof
-      fix i j k :: int have "(i + j) + k = i + (j + k)" by simp
-      then show "(i \<otimes> j) \<otimes> k = i \<otimes> (j \<otimes> k)"
-	unfolding mult_int_def .
-    qed
+instance %quote proof
+  fix i j k :: int have "(i + j) + k = i + (j + k)" by simp
+  then show "(i \<otimes> j) \<otimes> k = i \<otimes> (j \<otimes> k)"
+  unfolding mult_int_def .
+qed
 
-    end
+end %quote
 
 text {*
-  \noindent @{text "\<INSTANTIATION>"} allows to define class parameters
+  \noindent @{command instantiation} allows to define class parameters
   at a particular instance using common specification tools (here,
-  @{text "\<DEFINITION>"}).  The concluding @{text "\<INSTANCE>"}
+  @{command definition}).  The concluding @{command instance}
   opens a proof that the given parameters actually conform
   to the class specification.  Note that the first proof step
-  is the @{text default} method,
-  which for such instance proofs maps to the @{text intro_classes} method.
+  is the @{method default} method,
+  which for such instance proofs maps to the @{method intro_classes} method.
   This boils down an instance judgement to the relevant primitive
   proof goals and should conveniently always be the first method applied
   in an instantiation proof.
 
-  From now on, the type-checker will consider @{text "int"}
-  as a @{text "semigroup"} automatically, i.e.\ any general results
+  From now on, the type-checker will consider @{typ int}
+  as a @{class semigroup} automatically, i.e.\ any general results
   are immediately available on concrete instances.
-  \medskip Another instance of @{text "semigroup"} are the natural numbers:
+
+  \medskip Another instance of @{class semigroup} are the natural numbers:
 *}
 
-    instantiation nat :: semigroup
-    begin
+instantiation %quote nat :: semigroup
+begin
 
-    primrec mult_nat where
-      "(0\<Colon>nat) \<otimes> n = n"
-      | "Suc m \<otimes> n = Suc (m \<otimes> n)"
+primrec %quote mult_nat where
+  "(0\<Colon>nat) \<otimes> n = n"
+  | "Suc m \<otimes> n = Suc (m \<otimes> n)"
 
-    instance proof
-      fix m n q :: nat 
-      show "m \<otimes> n \<otimes> q = m \<otimes> (n \<otimes> q)"
-        by (induct m) auto
-    qed
+instance %quote proof
+  fix m n q :: nat 
+  show "m \<otimes> n \<otimes> q = m \<otimes> (n \<otimes> q)"
+    by (induct m) auto
+qed
 
-    end
+end %quote
 
 text {*
   \noindent Note the occurence of the name @{text mult_nat}
   in the primrec declaration;  by default, the local name of
   a class operation @{text f} to instantiate on type constructor
   @{text \<kappa>} are mangled as @{text f_\<kappa>}.  In case of uncertainty,
-  these names may be inspected using the @{text "\<PRINTCONTEXT>"} command
+  these names may be inspected using the @{command "print_context"} command
   or the corresponding ProofGeneral button.
 *}
 
@@ -222,27 +198,27 @@
   using our simple algebra:
 *}
 
-    instantiation * :: (semigroup, semigroup) semigroup
-    begin
+instantiation %quote * :: (semigroup, semigroup) semigroup
+begin
 
-    definition
-      mult_prod_def: "p\<^isub>1 \<otimes> p\<^isub>2 = (fst p\<^isub>1 \<otimes> fst p\<^isub>2, snd p\<^isub>1 \<otimes> snd p\<^isub>2)"
+definition %quote
+  mult_prod_def: "p\<^isub>1 \<otimes> p\<^isub>2 = (fst p\<^isub>1 \<otimes> fst p\<^isub>2, snd p\<^isub>1 \<otimes> snd p\<^isub>2)"
 
-    instance proof
-      fix p\<^isub>1 p\<^isub>2 p\<^isub>3 :: "\<alpha>\<Colon>semigroup \<times> \<beta>\<Colon>semigroup"
-      show "p\<^isub>1 \<otimes> p\<^isub>2 \<otimes> p\<^isub>3 = p\<^isub>1 \<otimes> (p\<^isub>2 \<otimes> p\<^isub>3)"
-	unfolding mult_prod_def by (simp add: assoc)
-    qed      
+instance %quote proof
+  fix p\<^isub>1 p\<^isub>2 p\<^isub>3 :: "\<alpha>\<Colon>semigroup \<times> \<beta>\<Colon>semigroup"
+  show "p\<^isub>1 \<otimes> p\<^isub>2 \<otimes> p\<^isub>3 = p\<^isub>1 \<otimes> (p\<^isub>2 \<otimes> p\<^isub>3)"
+  unfolding mult_prod_def by (simp add: assoc)
+qed      
 
-    end
+end %quote
 
 text {*
   \noindent Associativity from product semigroups is
   established using
-  the definition of @{text \<otimes>} on products and the hypothetical
+  the definition of @{text "(\<otimes>)"} on products and the hypothetical
   associativity of the type components;  these hypotheses
-  are facts due to the @{text semigroup} constraints imposed
-  on the type components by the @{text instance} proposition.
+  are facts due to the @{class semigroup} constraints imposed
+  on the type components by the @{command instance} proposition.
   Indeed, this pattern often occurs with parametric types
   and type classes.
 *}
@@ -251,15 +227,15 @@
 subsection {* Subclassing *}
 
 text {*
-  We define a subclass @{text "monoidl"} (a semigroup with a left-hand neutral)
-  by extending @{text "semigroup"}
-  with one additional parameter @{text "neutral"} together
+  We define a subclass @{text monoidl} (a semigroup with a left-hand neutral)
+  by extending @{class semigroup}
+  with one additional parameter @{text neutral} together
   with its property:
 *}
 
-    class monoidl = semigroup +
-      fixes neutral :: "\<alpha>" ("\<one>")
-      assumes neutl: "\<one> \<otimes> x = x"
+class %quote monoidl = semigroup +
+  fixes neutral :: "\<alpha>" ("\<one>")
+  assumes neutl: "\<one> \<otimes> x = x"
 
 text {*
   \noindent Again, we prove some instances, by
@@ -338,7 +314,7 @@
     end
 
 text {*
-  \noindent To finish our small algebra example, we add a @{text "group"} class
+  \noindent To finish our small algebra example, we add a @{text group} class
   with a corresponding instance:
 *}
 
@@ -379,7 +355,9 @@
 text {*
   \noindent essentially introduces the locale
 *}
-(*<*) setup {* Sign.add_path "foo" *} (*>*)
+
+setup %invisible {* Sign.add_path "foo" *}
+
 locale idem =
   fixes f :: "\<alpha> \<Rightarrow> \<alpha>"
   assumes idem: "f (f x) = f x"
@@ -401,7 +379,9 @@
 interpretation idem_class:
   idem ["f \<Colon> (\<alpha>\<Colon>idem) \<Rightarrow> \<alpha>"]
 by unfold_locales (rule idem)
-(*<*) setup {* Sign.parent_path *} (*>*)
+
+setup %invisible {* Sign.parent_path *}
+
 text {*
   This give you at hand the full power of the Isabelle module system;
   conclusions in locale @{text idem} are implicitly propagated
@@ -429,9 +409,9 @@
     qed
 
 text {*
-  \noindent Here the \qt{@{text "\<IN> group"}} target specification
+  \noindent Here the \qt{@{keyword "in"} @{class group}} target specification
   indicates that the result is recorded within that context for later
-  use.  This local theorem is also lifted to the global one @{text
+  use.  This local theorem is also lifted to the global one @{fact
   "group.left_cancel:"} @{prop [source] "\<And>x y z \<Colon> \<alpha>\<Colon>group. x \<otimes> y = x \<otimes>
   z \<longleftrightarrow> y = z"}.  Since type @{text "int"} has been made an instance of
   @{text "group"} before, we may refer to that fact as well: @{prop
@@ -474,15 +454,15 @@
   classes essentially correspond to functors which have
   a canonical interpretation as type classes.
   Anyway, there is also the possibility of other interpretations.
-  For example, also @{text "list"}s form a monoid with
-  @{term "op @"} and @{term "[]"} as operations, but it
+  For example, also @{text list}s form a monoid with
+  @{text append} and @{term "[]"} as operations, but it
   seems inappropriate to apply to lists
   the same operations as for genuinely algebraic types.
   In such a case, we simply can do a particular interpretation
   of monoids for lists:
 *}
 
-    interpretation list_monoid: monoid ["op @" "[]"]
+    interpretation list_monoid: monoid [append "[]"]
       by unfold_locales auto
 
 text {*
@@ -497,14 +477,14 @@
       "replicate 0 _ = []"
       | "replicate (Suc n) xs = xs @ replicate n xs"
 
-    interpretation list_monoid: monoid ["op @" "[]"] where
-      "monoid.pow_nat (op @) [] = replicate"
+    interpretation list_monoid: monoid [append "[]"] where
+      "monoid.pow_nat append [] = replicate"
     proof -
-      interpret monoid ["op @" "[]"] ..
-      show "monoid.pow_nat (op @) [] = replicate"
+      interpret monoid [append "[]"] ..
+      show "monoid.pow_nat append [] = replicate"
       proof
         fix n
-        show "monoid.pow_nat (op @) [] n = replicate n"
+        show "monoid.pow_nat append [] n = replicate n"
           by (induct n) auto
       qed
     qed intro_locales
@@ -571,11 +551,10 @@
   in @{text group} which uses @{text pow_nat}:
 *}
 
-    definition (in group)
-      pow_int :: "int \<Rightarrow> \<alpha> \<Rightarrow> \<alpha>" where
-      "pow_int k x = (if k >= 0
-        then pow_nat (nat k) x
-        else (pow_nat (nat (- k)) x)\<div>)"
+definition %quote (in group) pow_int :: "int \<Rightarrow> \<alpha> \<Rightarrow> \<alpha>" where
+  "pow_int k x = (if k >= 0
+    then pow_nat (nat k) x
+    else (pow_nat (nat (- k)) x)\<div>)"
 
 text {*
   \noindent yields the global definition of
@@ -591,15 +570,15 @@
   uniformly;  type inference resolves ambiguities.  For example:
 *}
 
-context semigroup
+context %quote semigroup
 begin
 
-term "x \<otimes> y" -- {* example 1 *}
-term "(x\<Colon>nat) \<otimes> y" -- {* example 2 *}
+term %quote "x \<otimes> y" -- {* example 1 *}
+term %quote "(x\<Colon>nat) \<otimes> y" -- {* example 2 *}
 
 end
 
-term "x \<otimes> y" -- {* example 3 *}
+term %quote "x \<otimes> y" -- {* example 3 *}
 
 text {*
   \noindent Here in example 1, the term refers to the local class operation
@@ -614,8 +593,8 @@
 text {*
   Turning back to the first motivation for type classes,
   namely overloading, it is obvious that overloading
-  stemming from @{text "\<CLASS>"} statements and
-  @{text "\<INSTANTIATION>"}
+  stemming from @{command class} statements and
+  @{command instantiation}
   targets naturally maps to Haskell type classes.
   The code generator framework \cite{isabelle-codegen} 
   takes this into account.  Concerning target languages
@@ -624,20 +603,19 @@
   As example, let's go back to the power function:
 *}
 
-    definition
-      example :: int where
-      "example = pow_int 10 (-2)"
+definition %quote example :: int where
+  "example = pow_int 10 (-2)"
 
 text {*
   \noindent This maps to Haskell as:
 *}
 
-text %quoteme {*@{code_stmts example (Haskell)}*}
+text %quote {*@{code_stmts example (Haskell)}*}
 
 text {*
   \noindent The whole code in SML with explicit dictionary passing:
 *}
 
-text %quoteme {*@{code_stmts example (SML)}*}
+text %quote {*@{code_stmts example (SML)}*}
 
 end
diff -r 1358b1ddd915 -r 519b17118926 doc-src/IsarAdvanced/Classes/Thy/ROOT.ML
--- a/doc-src/IsarAdvanced/Classes/Thy/ROOT.ML	Fri Oct 10 15:23:33 2008 +0200
+++ b/doc-src/IsarAdvanced/Classes/Thy/ROOT.ML	Fri Oct 10 15:52:45 2008 +0200
@@ -1,4 +1,6 @@
 
 (* $Id$ *)
 
+no_document use_thy "Setup";
+
 use_thy "Classes";
diff -r 1358b1ddd915 -r 519b17118926 doc-src/IsarAdvanced/Classes/Thy/Setup.thy
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/doc-src/IsarAdvanced/Classes/Thy/Setup.thy	Fri Oct 10 15:52:45 2008 +0200
@@ -0,0 +1,34 @@
+theory Setup
+imports Main Code_Integer
+uses
+  "../../../antiquote_setup"
+  "../../../more_antiquote"
+begin
+
+ML {* Code_Target.code_width := 74 *}
+
+syntax
+  "_alpha" :: "type"  ("\<alpha>")
+  "_alpha_ofsort" :: "sort \<Rightarrow> type"  ("\<alpha>()\<Colon>_" [0] 1000)
+  "_beta" :: "type"  ("\<beta>")
+  "_beta_ofsort" :: "sort \<Rightarrow> type"  ("\<beta>()\<Colon>_" [0] 1000)
+
+parse_ast_translation {*
+  let
+    fun alpha_ast_tr [] = Syntax.Variable "'a"
+      | alpha_ast_tr asts = raise Syntax.AST ("alpha_ast_tr", asts);
+    fun alpha_ofsort_ast_tr [ast] =
+      Syntax.Appl [Syntax.Constant "_ofsort", Syntax.Variable "'a", ast]
+      | alpha_ofsort_ast_tr asts = raise Syntax.AST ("alpha_ast_tr", asts);
+    fun beta_ast_tr [] = Syntax.Variable "'b"
+      | beta_ast_tr asts = raise Syntax.AST ("beta_ast_tr", asts);
+    fun beta_ofsort_ast_tr [ast] =
+      Syntax.Appl [Syntax.Constant "_ofsort", Syntax.Variable "'b", ast]
+      | beta_ofsort_ast_tr asts = raise Syntax.AST ("beta_ast_tr", asts);
+  in [
+    ("_alpha", alpha_ast_tr), ("_alpha_ofsort", alpha_ofsort_ast_tr),
+    ("_beta", beta_ast_tr), ("_beta_ofsort", beta_ofsort_ast_tr)
+  ] end
+*}
+
+end
\ No newline at end of file
diff -r 1358b1ddd915 -r 519b17118926 doc-src/IsarAdvanced/Classes/Thy/document/Classes.tex
--- a/doc-src/IsarAdvanced/Classes/Thy/document/Classes.tex	Fri Oct 10 15:23:33 2008 +0200
+++ b/doc-src/IsarAdvanced/Classes/Thy/document/Classes.tex	Fri Oct 10 15:52:45 2008 +0200
@@ -3,12 +3,14 @@
 \def\isabellecontext{Classes}%
 %
 \isadelimtheory
-\isanewline
 %
 \endisadelimtheory
 %
 \isatagtheory
-%
+\isacommand{theory}\isamarkupfalse%
+\ Classes\isanewline
+\isakeyword{imports}\ Main\ Setup\isanewline
+\isakeyword{begin}%
 \endisatagtheory
 {\isafoldtheory}%
 %
@@ -16,32 +18,6 @@
 %
 \endisadelimtheory
 %
-\isadelimML
-%
-\endisadelimML
-%
-\isatagML
-%
-\endisatagML
-{\isafoldML}%
-%
-\isadelimML
-%
-\endisadelimML
-%
-\isadelimML
-%
-\endisadelimML
-%
-\isatagML
-%
-\endisatagML
-{\isafoldML}%
-%
-\isadelimML
-%
-\endisadelimML
-%
 \isamarkupchapter{Haskell-style classes with Isabelle/Isar%
 }
 \isamarkuptrue%
@@ -62,23 +38,27 @@
   of the \isa{eq} function from its overloaded definitions by means
   of \isa{class} and \isa{instance} declarations:
 
-  \medskip\noindent\hspace*{2ex}\isa{class\ eq\ where}\footnote{syntax here is a kind of isabellized Haskell} \\
-  \hspace*{4ex}\isa{eq\ {\isasymColon}\ {\isasymalpha}\ {\isasymRightarrow}\ {\isasymalpha}\ {\isasymRightarrow}\ bool}
+  \begin{quote}
+
+  \noindent\isa{class\ eq\ where}\footnote{syntax here is a kind of isabellized Haskell} \\
+  \hspace*{2ex}\isa{eq\ {\isasymColon}\ {\isasymalpha}\ {\isasymRightarrow}\ {\isasymalpha}\ {\isasymRightarrow}\ bool}
 
-  \medskip\noindent\hspace*{2ex}\isa{instance\ nat\ {\isasymColon}\ eq\ where} \\
-  \hspace*{4ex}\isa{eq\ {\isadigit{0}}\ {\isadigit{0}}\ {\isacharequal}\ True} \\
-  \hspace*{4ex}\isa{eq\ {\isadigit{0}}\ {\isacharunderscore}\ {\isacharequal}\ False} \\
-  \hspace*{4ex}\isa{eq\ {\isacharunderscore}\ {\isadigit{0}}\ {\isacharequal}\ False} \\
-  \hspace*{4ex}\isa{eq\ {\isacharparenleft}Suc\ n{\isacharparenright}\ {\isacharparenleft}Suc\ m{\isacharparenright}\ {\isacharequal}\ eq\ n\ m}
+  \medskip\noindent\isa{instance\ nat\ {\isasymColon}\ eq\ where} \\
+  \hspace*{2ex}\isa{eq\ {\isadigit{0}}\ {\isadigit{0}}\ {\isacharequal}\ True} \\
+  \hspace*{2ex}\isa{eq\ {\isadigit{0}}\ {\isacharunderscore}\ {\isacharequal}\ False} \\
+  \hspace*{2ex}\isa{eq\ {\isacharunderscore}\ {\isadigit{0}}\ {\isacharequal}\ False} \\
+  \hspace*{2ex}\isa{eq\ {\isacharparenleft}Suc\ n{\isacharparenright}\ {\isacharparenleft}Suc\ m{\isacharparenright}\ {\isacharequal}\ eq\ n\ m}
 
-  \medskip\noindent\hspace*{2ex}\isa{instance\ {\isacharparenleft}{\isasymalpha}{\isasymColon}eq{\isacharcomma}\ {\isasymbeta}{\isasymColon}eq{\isacharparenright}\ pair\ {\isasymColon}\ eq\ where} \\
-  \hspace*{4ex}\isa{eq\ {\isacharparenleft}x{\isadigit{1}}{\isacharcomma}\ y{\isadigit{1}}{\isacharparenright}\ {\isacharparenleft}x{\isadigit{2}}{\isacharcomma}\ y{\isadigit{2}}{\isacharparenright}\ {\isacharequal}\ eq\ x{\isadigit{1}}\ x{\isadigit{2}}\ {\isasymand}\ eq\ y{\isadigit{1}}\ y{\isadigit{2}}}
+  \medskip\noindent\\isa{instance\ {\isacharparenleft}{\isasymalpha}{\isasymColon}eq{\isacharcomma}\ {\isasymbeta}{\isasymColon}eq{\isacharparenright}\ pair\ {\isasymColon}\ eq\ where} \\
+  \hspace*{2ex}\isa{eq\ {\isacharparenleft}x{\isadigit{1}}{\isacharcomma}\ y{\isadigit{1}}{\isacharparenright}\ {\isacharparenleft}x{\isadigit{2}}{\isacharcomma}\ y{\isadigit{2}}{\isacharparenright}\ {\isacharequal}\ eq\ x{\isadigit{1}}\ x{\isadigit{2}}\ {\isasymand}\ eq\ y{\isadigit{1}}\ y{\isadigit{2}}}
 
-  \medskip\noindent\hspace*{2ex}\isa{class\ ord\ extends\ eq\ where} \\
-  \hspace*{4ex}\isa{less{\isacharunderscore}eq\ {\isasymColon}\ {\isasymalpha}\ {\isasymRightarrow}\ {\isasymalpha}\ {\isasymRightarrow}\ bool} \\
-  \hspace*{4ex}\isa{less\ {\isasymColon}\ {\isasymalpha}\ {\isasymRightarrow}\ {\isasymalpha}\ {\isasymRightarrow}\ bool}
+  \medskip\noindent\isa{class\ ord\ extends\ eq\ where} \\
+  \hspace*{2ex}\isa{less{\isacharunderscore}eq\ {\isasymColon}\ {\isasymalpha}\ {\isasymRightarrow}\ {\isasymalpha}\ {\isasymRightarrow}\ bool} \\
+  \hspace*{2ex}\isa{less\ {\isasymColon}\ {\isasymalpha}\ {\isasymRightarrow}\ {\isasymalpha}\ {\isasymRightarrow}\ bool}
 
-  \medskip\noindent Type variables are annotated with (finitely many) classes;
+  \end{quote}
+
+  \noindent Type variables are annotated with (finitely many) classes;
   these annotations are assertions that a particular polymorphic type
   provides definitions for overloaded functions.
 
@@ -95,14 +75,18 @@
   \isa{class\ eq} is an equivalence relation obeying reflexivity,
   symmetry and transitivity:
 
-  \medskip\noindent\hspace*{2ex}\isa{class\ eq\ where} \\
-  \hspace*{4ex}\isa{eq\ {\isasymColon}\ {\isasymalpha}\ {\isasymRightarrow}\ {\isasymalpha}\ {\isasymRightarrow}\ bool} \\
-  \hspace*{2ex}\isa{satisfying} \\
-  \hspace*{4ex}\isa{refl{\isacharcolon}\ eq\ x\ x} \\
-  \hspace*{4ex}\isa{sym{\isacharcolon}\ eq\ x\ y\ {\isasymlongleftrightarrow}\ eq\ x\ y} \\
-  \hspace*{4ex}\isa{trans{\isacharcolon}\ eq\ x\ y\ {\isasymand}\ eq\ y\ z\ {\isasymlongrightarrow}\ eq\ x\ z}
+  \begin{quote}
 
-  \medskip\noindent From a theoretic point of view, type classes are lightweight
+  \noindent\isa{class\ eq\ where} \\
+  \hspace*{2ex}\isa{eq\ {\isasymColon}\ {\isasymalpha}\ {\isasymRightarrow}\ {\isasymalpha}\ {\isasymRightarrow}\ bool} \\
+  \isa{satisfying} \\
+  \hspace*{2ex}\isa{refl{\isacharcolon}\ eq\ x\ x} \\
+  \hspace*{2ex}\isa{sym{\isacharcolon}\ eq\ x\ y\ {\isasymlongleftrightarrow}\ eq\ x\ y} \\
+  \hspace*{2ex}\isa{trans{\isacharcolon}\ eq\ x\ y\ {\isasymand}\ eq\ y\ z\ {\isasymlongrightarrow}\ eq\ x\ z}
+
+  \end{quote}
+
+  \noindent From a theoretic point of view, type classes are lightweight
   modules; Haskell type classes may be emulated by
   SML functors \cite{classes_modules}. 
   Isabelle/Isar offers a discipline of type classes which brings
@@ -142,20 +126,36 @@
 \isamarkuptrue%
 %
 \begin{isamarkuptext}%
-Depending on an arbitrary type \isa{{\isasymalpha}}, class \isa{semigroup} introduces a binary operator \isa{{\isasymotimes}} that is
+Depending on an arbitrary type \isa{{\isasymalpha}}, class \isa{semigroup} introduces a binary operator \isa{{\isacharparenleft}{\isasymotimes}{\isacharparenright}} that is
   assumed to be associative:%
 \end{isamarkuptext}%
 \isamarkuptrue%
-\ \ \ \ \isacommand{class}\isamarkupfalse%
+%
+\isadelimquote
+%
+\endisadelimquote
+%
+\isatagquote
+\isacommand{class}\isamarkupfalse%
 \ semigroup\ {\isacharequal}\ type\ {\isacharplus}\isanewline
-\ \ \ \ \ \ \isakeyword{fixes}\ mult\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequoteopen}{\isasymalpha}\ {\isasymRightarrow}\ {\isasymalpha}\ {\isasymRightarrow}\ {\isasymalpha}{\isachardoublequoteclose}\ \ \ \ {\isacharparenleft}\isakeyword{infixl}\ {\isachardoublequoteopen}{\isasymotimes}{\isachardoublequoteclose}\ {\isadigit{7}}{\isadigit{0}}{\isacharparenright}\isanewline
-\ \ \ \ \ \ \isakeyword{assumes}\ assoc{\isacharcolon}\ {\isachardoublequoteopen}{\isacharparenleft}x\ {\isasymotimes}\ y{\isacharparenright}\ {\isasymotimes}\ z\ {\isacharequal}\ x\ {\isasymotimes}\ {\isacharparenleft}y\ {\isasymotimes}\ z{\isacharparenright}{\isachardoublequoteclose}%
+\ \ \isakeyword{fixes}\ mult\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequoteopen}{\isasymalpha}\ {\isasymRightarrow}\ {\isasymalpha}\ {\isasymRightarrow}\ {\isasymalpha}{\isachardoublequoteclose}\ \ \ \ {\isacharparenleft}\isakeyword{infixl}\ {\isachardoublequoteopen}{\isasymotimes}{\isachardoublequoteclose}\ {\isadigit{7}}{\isadigit{0}}{\isacharparenright}\isanewline
+\ \ \isakeyword{assumes}\ assoc{\isacharcolon}\ {\isachardoublequoteopen}{\isacharparenleft}x\ {\isasymotimes}\ y{\isacharparenright}\ {\isasymotimes}\ z\ {\isacharequal}\ x\ {\isasymotimes}\ {\isacharparenleft}y\ {\isasymotimes}\ z{\isacharparenright}{\isachardoublequoteclose}%
+\endisatagquote
+{\isafoldquote}%
+%
+\isadelimquote
+%
+\endisadelimquote
+%
 \begin{isamarkuptext}%
-\noindent This \isa{{\isasymCLASS}} specification consists of two
-  parts: the \qn{operational} part names the class parameter (\isa{{\isasymFIXES}}), the \qn{logical} part specifies properties on them
-  (\isa{{\isasymASSUMES}}).  The local \isa{{\isasymFIXES}} and \isa{{\isasymASSUMES}} are lifted to the theory toplevel, yielding the global
+\noindent This \hyperlink{command.class}{\mbox{\isa{\isacommand{class}}}} specification consists of two
+  parts: the \qn{operational} part names the class parameter
+  (\hyperlink{element.fixes}{\mbox{\isa{\isakeyword{fixes}}}}), the \qn{logical} part specifies properties on them
+  (\hyperlink{element.assumes}{\mbox{\isa{\isakeyword{assumes}}}}).  The local \hyperlink{element.fixes}{\mbox{\isa{\isakeyword{fixes}}}} and
+  \hyperlink{element.assumes}{\mbox{\isa{\isakeyword{assumes}}}} are lifted to the theory toplevel,
+  yielding the global
   parameter \isa{{\isachardoublequote}mult\ {\isasymColon}\ {\isasymalpha}{\isasymColon}semigroup\ {\isasymRightarrow}\ {\isasymalpha}\ {\isasymRightarrow}\ {\isasymalpha}{\isachardoublequote}} and the
-  global theorem \isa{semigroup{\isachardot}assoc{\isacharcolon}}~\isa{{\isachardoublequote}{\isasymAnd}x\ y\ z\ {\isasymColon}\ {\isasymalpha}{\isasymColon}semigroup{\isachardot}\ {\isacharparenleft}x\ {\isasymotimes}\ y{\isacharparenright}\ {\isasymotimes}\ z\ {\isacharequal}\ x\ {\isasymotimes}\ {\isacharparenleft}y\ {\isasymotimes}\ z{\isacharparenright}{\isachardoublequote}}.%
+  global theorem \hyperlink{fact.semigroup.assoc:}{\mbox{\isa{semigroup{\isachardot}assoc{\isacharcolon}}}}~\isa{{\isachardoublequote}{\isasymAnd}x\ y\ z\ {\isasymColon}\ {\isasymalpha}{\isasymColon}semigroup{\isachardot}\ {\isacharparenleft}x\ {\isasymotimes}\ y{\isacharparenright}\ {\isasymotimes}\ z\ {\isacharequal}\ x\ {\isasymotimes}\ {\isacharparenleft}y\ {\isasymotimes}\ z{\isacharparenright}{\isachardoublequote}}.%
 \end{isamarkuptext}%
 \isamarkuptrue%
 %
@@ -166,57 +166,57 @@
 \begin{isamarkuptext}%
 The concrete type \isa{int} is made a \isa{semigroup}
   instance by providing a suitable definition for the class parameter
-  \isa{mult} and a proof for the specification of \isa{assoc}.
-  This is accomplished by the \isa{{\isasymINSTANTIATION}} target:%
+  \isa{{\isacharparenleft}{\isasymotimes}{\isacharparenright}} and a proof for the specification of \hyperlink{fact.assoc}{\mbox{\isa{assoc}}}.
+  This is accomplished by the \hyperlink{command.instantiation}{\mbox{\isa{\isacommand{instantiation}}}} target:%
 \end{isamarkuptext}%
 \isamarkuptrue%
-\ \ \ \ \isacommand{instantiation}\isamarkupfalse%
+%
+\isadelimquote
+%
+\endisadelimquote
+%
+\isatagquote
+\isacommand{instantiation}\isamarkupfalse%
 \ int\ {\isacharcolon}{\isacharcolon}\ semigroup\isanewline
-\ \ \ \ \isakeyword{begin}\isanewline
-\isanewline
-\ \ \ \ \isacommand{definition}\isamarkupfalse%
-\isanewline
-\ \ \ \ \ \ mult{\isacharunderscore}int{\isacharunderscore}def{\isacharcolon}\ {\isachardoublequoteopen}i\ {\isasymotimes}\ j\ {\isacharequal}\ i\ {\isacharplus}\ {\isacharparenleft}j{\isasymColon}int{\isacharparenright}{\isachardoublequoteclose}\isanewline
+\isakeyword{begin}\isanewline
 \isanewline
-\ \ \ \ \isacommand{instance}\isamarkupfalse%
-%
-\isadelimproof
-\ %
-\endisadelimproof
-%
-\isatagproof
-\isacommand{proof}\isamarkupfalse%
+\isacommand{definition}\isamarkupfalse%
+\isanewline
+\ \ mult{\isacharunderscore}int{\isacharunderscore}def{\isacharcolon}\ {\isachardoublequoteopen}i\ {\isasymotimes}\ j\ {\isacharequal}\ i\ {\isacharplus}\ {\isacharparenleft}j{\isasymColon}int{\isacharparenright}{\isachardoublequoteclose}\isanewline
 \isanewline
-\ \ \ \ \ \ \isacommand{fix}\isamarkupfalse%
+\isacommand{instance}\isamarkupfalse%
+\ \isacommand{proof}\isamarkupfalse%
+\isanewline
+\ \ \isacommand{fix}\isamarkupfalse%
 \ i\ j\ k\ {\isacharcolon}{\isacharcolon}\ int\ \isacommand{have}\isamarkupfalse%
 \ {\isachardoublequoteopen}{\isacharparenleft}i\ {\isacharplus}\ j{\isacharparenright}\ {\isacharplus}\ k\ {\isacharequal}\ i\ {\isacharplus}\ {\isacharparenleft}j\ {\isacharplus}\ k{\isacharparenright}{\isachardoublequoteclose}\ \isacommand{by}\isamarkupfalse%
 \ simp\isanewline
-\ \ \ \ \ \ \isacommand{then}\isamarkupfalse%
+\ \ \isacommand{then}\isamarkupfalse%
 \ \isacommand{show}\isamarkupfalse%
 \ {\isachardoublequoteopen}{\isacharparenleft}i\ {\isasymotimes}\ j{\isacharparenright}\ {\isasymotimes}\ k\ {\isacharequal}\ i\ {\isasymotimes}\ {\isacharparenleft}j\ {\isasymotimes}\ k{\isacharparenright}{\isachardoublequoteclose}\isanewline
-\ \ \ \ \ \ \ \ \isacommand{unfolding}\isamarkupfalse%
+\ \ \isacommand{unfolding}\isamarkupfalse%
 \ mult{\isacharunderscore}int{\isacharunderscore}def\ \isacommand{{\isachardot}}\isamarkupfalse%
 \isanewline
-\ \ \ \ \isacommand{qed}\isamarkupfalse%
-%
-\endisatagproof
-{\isafoldproof}%
-%
-\isadelimproof
-%
-\endisadelimproof
+\isacommand{qed}\isamarkupfalse%
 \isanewline
 \isanewline
-\ \ \ \ \isacommand{end}\isamarkupfalse%
+\isacommand{end}\isamarkupfalse%
+%
+\endisatagquote
+{\isafoldquote}%
+%
+\isadelimquote
+%
+\endisadelimquote
 %
 \begin{isamarkuptext}%
-\noindent \isa{{\isasymINSTANTIATION}} allows to define class parameters
+\noindent \hyperlink{command.instantiation}{\mbox{\isa{\isacommand{instantiation}}}} allows to define class parameters
   at a particular instance using common specification tools (here,
-  \isa{{\isasymDEFINITION}}).  The concluding \isa{{\isasymINSTANCE}}
+  \hyperlink{command.definition}{\mbox{\isa{\isacommand{definition}}}}).  The concluding \hyperlink{command.instance}{\mbox{\isa{\isacommand{instance}}}}
   opens a proof that the given parameters actually conform
   to the class specification.  Note that the first proof step
-  is the \isa{default} method,
-  which for such instance proofs maps to the \isa{intro{\isacharunderscore}classes} method.
+  is the \hyperlink{method.default}{\mbox{\isa{default}}} method,
+  which for such instance proofs maps to the \hyperlink{method.intro-classes}{\mbox{\isa{intro{\isacharunderscore}classes}}} method.
   This boils down an instance judgement to the relevant primitive
   proof goals and should conveniently always be the first method applied
   in an instantiation proof.
@@ -224,51 +224,52 @@
   From now on, the type-checker will consider \isa{int}
   as a \isa{semigroup} automatically, i.e.\ any general results
   are immediately available on concrete instances.
+
   \medskip Another instance of \isa{semigroup} are the natural numbers:%
 \end{isamarkuptext}%
 \isamarkuptrue%
-\ \ \ \ \isacommand{instantiation}\isamarkupfalse%
-\ nat\ {\isacharcolon}{\isacharcolon}\ semigroup\isanewline
-\ \ \ \ \isakeyword{begin}\isanewline
-\isanewline
-\ \ \ \ \isacommand{primrec}\isamarkupfalse%
-\ mult{\isacharunderscore}nat\ \isakeyword{where}\isanewline
-\ \ \ \ \ \ {\isachardoublequoteopen}{\isacharparenleft}{\isadigit{0}}{\isasymColon}nat{\isacharparenright}\ {\isasymotimes}\ n\ {\isacharequal}\ n{\isachardoublequoteclose}\isanewline
-\ \ \ \ \ \ {\isacharbar}\ {\isachardoublequoteopen}Suc\ m\ {\isasymotimes}\ n\ {\isacharequal}\ Suc\ {\isacharparenleft}m\ {\isasymotimes}\ n{\isacharparenright}{\isachardoublequoteclose}\isanewline
-\isanewline
-\ \ \ \ \isacommand{instance}\isamarkupfalse%
 %
-\isadelimproof
-\ %
-\endisadelimproof
+\isadelimquote
+%
+\endisadelimquote
 %
-\isatagproof
-\isacommand{proof}\isamarkupfalse%
+\isatagquote
+\isacommand{instantiation}\isamarkupfalse%
+\ nat\ {\isacharcolon}{\isacharcolon}\ semigroup\isanewline
+\isakeyword{begin}\isanewline
 \isanewline
-\ \ \ \ \ \ \isacommand{fix}\isamarkupfalse%
+\isacommand{primrec}\isamarkupfalse%
+\ mult{\isacharunderscore}nat\ \isakeyword{where}\isanewline
+\ \ {\isachardoublequoteopen}{\isacharparenleft}{\isadigit{0}}{\isasymColon}nat{\isacharparenright}\ {\isasymotimes}\ n\ {\isacharequal}\ n{\isachardoublequoteclose}\isanewline
+\ \ {\isacharbar}\ {\isachardoublequoteopen}Suc\ m\ {\isasymotimes}\ n\ {\isacharequal}\ Suc\ {\isacharparenleft}m\ {\isasymotimes}\ n{\isacharparenright}{\isachardoublequoteclose}\isanewline
+\isanewline
+\isacommand{instance}\isamarkupfalse%
+\ \isacommand{proof}\isamarkupfalse%
+\isanewline
+\ \ \isacommand{fix}\isamarkupfalse%
 \ m\ n\ q\ {\isacharcolon}{\isacharcolon}\ nat\ \isanewline
-\ \ \ \ \ \ \isacommand{show}\isamarkupfalse%
+\ \ \isacommand{show}\isamarkupfalse%
 \ {\isachardoublequoteopen}m\ {\isasymotimes}\ n\ {\isasymotimes}\ q\ {\isacharequal}\ m\ {\isasymotimes}\ {\isacharparenleft}n\ {\isasymotimes}\ q{\isacharparenright}{\isachardoublequoteclose}\isanewline
-\ \ \ \ \ \ \ \ \isacommand{by}\isamarkupfalse%
+\ \ \ \ \isacommand{by}\isamarkupfalse%
 \ {\isacharparenleft}induct\ m{\isacharparenright}\ auto\isanewline
-\ \ \ \ \isacommand{qed}\isamarkupfalse%
-%
-\endisatagproof
-{\isafoldproof}%
-%
-\isadelimproof
-%
-\endisadelimproof
+\isacommand{qed}\isamarkupfalse%
 \isanewline
 \isanewline
-\ \ \ \ \isacommand{end}\isamarkupfalse%
+\isacommand{end}\isamarkupfalse%
+%
+\endisatagquote
+{\isafoldquote}%
+%
+\isadelimquote
+%
+\endisadelimquote
 %
 \begin{isamarkuptext}%
 \noindent Note the occurence of the name \isa{mult{\isacharunderscore}nat}
   in the primrec declaration;  by default, the local name of
   a class operation \isa{f} to instantiate on type constructor
   \isa{{\isasymkappa}} are mangled as \isa{f{\isacharunderscore}{\isasymkappa}}.  In case of uncertainty,
-  these names may be inspected using the \isa{{\isasymPRINTCONTEXT}} command
+  these names may be inspected using the \hyperlink{command.print-context}{\mbox{\isa{\isacommand{print{\isacharunderscore}context}}}} command
   or the corresponding ProofGeneral button.%
 \end{isamarkuptext}%
 \isamarkuptrue%
@@ -284,49 +285,49 @@
   using our simple algebra:%
 \end{isamarkuptext}%
 \isamarkuptrue%
-\ \ \ \ \isacommand{instantiation}\isamarkupfalse%
-\ {\isacharasterisk}\ {\isacharcolon}{\isacharcolon}\ {\isacharparenleft}semigroup{\isacharcomma}\ semigroup{\isacharparenright}\ semigroup\isanewline
-\ \ \ \ \isakeyword{begin}\isanewline
-\isanewline
-\ \ \ \ \isacommand{definition}\isamarkupfalse%
-\isanewline
-\ \ \ \ \ \ mult{\isacharunderscore}prod{\isacharunderscore}def{\isacharcolon}\ {\isachardoublequoteopen}p\isactrlisub {\isadigit{1}}\ {\isasymotimes}\ p\isactrlisub {\isadigit{2}}\ {\isacharequal}\ {\isacharparenleft}fst\ p\isactrlisub {\isadigit{1}}\ {\isasymotimes}\ fst\ p\isactrlisub {\isadigit{2}}{\isacharcomma}\ snd\ p\isactrlisub {\isadigit{1}}\ {\isasymotimes}\ snd\ p\isactrlisub {\isadigit{2}}{\isacharparenright}{\isachardoublequoteclose}\isanewline
-\isanewline
-\ \ \ \ \isacommand{instance}\isamarkupfalse%
+%
+\isadelimquote
+%
+\endisadelimquote
 %
-\isadelimproof
-\ %
-\endisadelimproof
-%
-\isatagproof
-\isacommand{proof}\isamarkupfalse%
+\isatagquote
+\isacommand{instantiation}\isamarkupfalse%
+\ {\isacharasterisk}\ {\isacharcolon}{\isacharcolon}\ {\isacharparenleft}semigroup{\isacharcomma}\ semigroup{\isacharparenright}\ semigroup\isanewline
+\isakeyword{begin}\isanewline
+\isanewline
+\isacommand{definition}\isamarkupfalse%
+\isanewline
+\ \ mult{\isacharunderscore}prod{\isacharunderscore}def{\isacharcolon}\ {\isachardoublequoteopen}p\isactrlisub {\isadigit{1}}\ {\isasymotimes}\ p\isactrlisub {\isadigit{2}}\ {\isacharequal}\ {\isacharparenleft}fst\ p\isactrlisub {\isadigit{1}}\ {\isasymotimes}\ fst\ p\isactrlisub {\isadigit{2}}{\isacharcomma}\ snd\ p\isactrlisub {\isadigit{1}}\ {\isasymotimes}\ snd\ p\isactrlisub {\isadigit{2}}{\isacharparenright}{\isachardoublequoteclose}\isanewline
 \isanewline
-\ \ \ \ \ \ \isacommand{fix}\isamarkupfalse%
+\isacommand{instance}\isamarkupfalse%
+\ \isacommand{proof}\isamarkupfalse%
+\isanewline
+\ \ \isacommand{fix}\isamarkupfalse%
 \ p\isactrlisub {\isadigit{1}}\ p\isactrlisub {\isadigit{2}}\ p\isactrlisub {\isadigit{3}}\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequoteopen}{\isasymalpha}{\isasymColon}semigroup\ {\isasymtimes}\ {\isasymbeta}{\isasymColon}semigroup{\isachardoublequoteclose}\isanewline
-\ \ \ \ \ \ \isacommand{show}\isamarkupfalse%
+\ \ \isacommand{show}\isamarkupfalse%
 \ {\isachardoublequoteopen}p\isactrlisub {\isadigit{1}}\ {\isasymotimes}\ p\isactrlisub {\isadigit{2}}\ {\isasymotimes}\ p\isactrlisub {\isadigit{3}}\ {\isacharequal}\ p\isactrlisub {\isadigit{1}}\ {\isasymotimes}\ {\isacharparenleft}p\isactrlisub {\isadigit{2}}\ {\isasymotimes}\ p\isactrlisub {\isadigit{3}}{\isacharparenright}{\isachardoublequoteclose}\isanewline
-\ \ \ \ \ \ \ \ \isacommand{unfolding}\isamarkupfalse%
+\ \ \isacommand{unfolding}\isamarkupfalse%
 \ mult{\isacharunderscore}prod{\isacharunderscore}def\ \isacommand{by}\isamarkupfalse%
 \ {\isacharparenleft}simp\ add{\isacharcolon}\ assoc{\isacharparenright}\isanewline
-\ \ \ \ \isacommand{qed}\isamarkupfalse%
-%
-\endisatagproof
-{\isafoldproof}%
-%
-\isadelimproof
-%
-\endisadelimproof
+\isacommand{qed}\isamarkupfalse%
 \ \ \ \ \ \ \isanewline
 \isanewline
-\ \ \ \ \isacommand{end}\isamarkupfalse%
+\isacommand{end}\isamarkupfalse%
+%
+\endisatagquote
+{\isafoldquote}%
+%
+\isadelimquote
+%
+\endisadelimquote
 %
 \begin{isamarkuptext}%
 \noindent Associativity from product semigroups is
   established using
-  the definition of \isa{{\isasymotimes}} on products and the hypothetical
+  the definition of \isa{{\isacharparenleft}{\isasymotimes}{\isacharparenright}} on products and the hypothetical
   associativity of the type components;  these hypotheses
   are facts due to the \isa{semigroup} constraints imposed
-  on the type components by the \isa{instance} proposition.
+  on the type components by the \hyperlink{command.instance}{\mbox{\isa{\isacommand{instance}}}} proposition.
   Indeed, this pattern often occurs with parametric types
   and type classes.%
 \end{isamarkuptext}%
@@ -343,10 +344,23 @@
   with its property:%
 \end{isamarkuptext}%
 \isamarkuptrue%
-\ \ \ \ \isacommand{class}\isamarkupfalse%
+%
+\isadelimquote
+%
+\endisadelimquote
+%
+\isatagquote
+\isacommand{class}\isamarkupfalse%
 \ monoidl\ {\isacharequal}\ semigroup\ {\isacharplus}\isanewline
-\ \ \ \ \ \ \isakeyword{fixes}\ neutral\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequoteopen}{\isasymalpha}{\isachardoublequoteclose}\ {\isacharparenleft}{\isachardoublequoteopen}{\isasymone}{\isachardoublequoteclose}{\isacharparenright}\isanewline
-\ \ \ \ \ \ \isakeyword{assumes}\ neutl{\isacharcolon}\ {\isachardoublequoteopen}{\isasymone}\ {\isasymotimes}\ x\ {\isacharequal}\ x{\isachardoublequoteclose}%
+\ \ \isakeyword{fixes}\ neutral\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequoteopen}{\isasymalpha}{\isachardoublequoteclose}\ {\isacharparenleft}{\isachardoublequoteopen}{\isasymone}{\isachardoublequoteclose}{\isacharparenright}\isanewline
+\ \ \isakeyword{assumes}\ neutl{\isacharcolon}\ {\isachardoublequoteopen}{\isasymone}\ {\isasymotimes}\ x\ {\isacharequal}\ x{\isachardoublequoteclose}%
+\endisatagquote
+{\isafoldquote}%
+%
+\isadelimquote
+%
+\endisadelimquote
+%
 \begin{isamarkuptext}%
 \noindent Again, we prove some instances, by
   providing suitable parameter definitions and proofs for the
@@ -597,18 +611,21 @@
 \end{isamarkuptext}%
 \isamarkuptrue%
 %
-\isadelimML
+\isadeliminvisible
 %
-\endisadelimML
-%
-\isatagML
+\endisadeliminvisible
 %
-\endisatagML
-{\isafoldML}%
+\isataginvisible
+\isacommand{setup}\isamarkupfalse%
+\ {\isacharverbatimopen}\ Sign{\isachardot}add{\isacharunderscore}path\ {\isachardoublequote}foo{\isachardoublequote}\ {\isacharverbatimclose}%
+\endisataginvisible
+{\isafoldinvisible}%
 %
-\isadelimML
+\isadeliminvisible
 %
-\endisadelimML
+\endisadeliminvisible
+\isanewline
+\isanewline
 \isacommand{locale}\isamarkupfalse%
 \ idem\ {\isacharequal}\isanewline
 \ \ \isakeyword{fixes}\ f\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequoteopen}{\isasymalpha}\ {\isasymRightarrow}\ {\isasymalpha}{\isachardoublequoteclose}\isanewline
@@ -646,21 +663,24 @@
 {\isafoldproof}%
 %
 \isadelimproof
+\isanewline
 %
 \endisadelimproof
 %
-\isadelimML
+\isadeliminvisible
+\isanewline
 %
-\endisadelimML
-%
-\isatagML
+\endisadeliminvisible
 %
-\endisatagML
-{\isafoldML}%
+\isataginvisible
+\isacommand{setup}\isamarkupfalse%
+\ {\isacharverbatimopen}\ Sign{\isachardot}parent{\isacharunderscore}path\ {\isacharverbatimclose}%
+\endisataginvisible
+{\isafoldinvisible}%
 %
-\isadelimML
+\isadeliminvisible
 %
-\endisadelimML
+\endisadeliminvisible
 %
 \begin{isamarkuptext}%
 This give you at hand the full power of the Isabelle module system;
@@ -724,9 +744,9 @@
 \endisadelimproof
 %
 \begin{isamarkuptext}%
-\noindent Here the \qt{\isa{{\isasymIN}\ group}} target specification
+\noindent Here the \qt{\hyperlink{keyword.in}{\mbox{\isa{\isakeyword{in}}}} \isa{group}} target specification
   indicates that the result is recorded within that context for later
-  use.  This local theorem is also lifted to the global one \isa{group{\isachardot}left{\isacharunderscore}cancel{\isacharcolon}} \isa{{\isachardoublequote}{\isasymAnd}x\ y\ z\ {\isasymColon}\ {\isasymalpha}{\isasymColon}group{\isachardot}\ x\ {\isasymotimes}\ y\ {\isacharequal}\ x\ {\isasymotimes}\ z\ {\isasymlongleftrightarrow}\ y\ {\isacharequal}\ z{\isachardoublequote}}.  Since type \isa{int} has been made an instance of
+  use.  This local theorem is also lifted to the global one \hyperlink{fact.group.left-cancel:}{\mbox{\isa{group{\isachardot}left{\isacharunderscore}cancel{\isacharcolon}}}} \isa{{\isachardoublequote}{\isasymAnd}x\ y\ z\ {\isasymColon}\ {\isasymalpha}{\isasymColon}group{\isachardot}\ x\ {\isasymotimes}\ y\ {\isacharequal}\ x\ {\isasymotimes}\ z\ {\isasymlongleftrightarrow}\ y\ {\isacharequal}\ z{\isachardoublequote}}.  Since type \isa{int} has been made an instance of
   \isa{group} before, we may refer to that fact as well: \isa{{\isachardoublequote}{\isasymAnd}x\ y\ z\ {\isasymColon}\ int{\isachardot}\ x\ {\isasymotimes}\ y\ {\isacharequal}\ x\ {\isasymotimes}\ z\ {\isasymlongleftrightarrow}\ y\ {\isacharequal}\ z{\isachardoublequote}}.%
 \end{isamarkuptext}%
 \isamarkuptrue%
@@ -772,7 +792,7 @@
   a canonical interpretation as type classes.
   Anyway, there is also the possibility of other interpretations.
   For example, also \isa{list}s form a monoid with
-  \isa{op\ {\isacharat}} and \isa{{\isacharbrackleft}{\isacharbrackright}} as operations, but it
+  \isa{append} and \isa{{\isacharbrackleft}{\isacharbrackright}} as operations, but it
   seems inappropriate to apply to lists
   the same operations as for genuinely algebraic types.
   In such a case, we simply can do a particular interpretation
@@ -780,7 +800,7 @@
 \end{isamarkuptext}%
 \isamarkuptrue%
 \ \ \ \ \isacommand{interpretation}\isamarkupfalse%
-\ list{\isacharunderscore}monoid{\isacharcolon}\ monoid\ {\isacharbrackleft}{\isachardoublequoteopen}op\ {\isacharat}{\isachardoublequoteclose}\ {\isachardoublequoteopen}{\isacharbrackleft}{\isacharbrackright}{\isachardoublequoteclose}{\isacharbrackright}\isanewline
+\ list{\isacharunderscore}monoid{\isacharcolon}\ monoid\ {\isacharbrackleft}append\ {\isachardoublequoteopen}{\isacharbrackleft}{\isacharbrackright}{\isachardoublequoteclose}{\isacharbrackright}\isanewline
 %
 \isadelimproof
 \ \ \ \ \ \ %
@@ -810,8 +830,8 @@
 \ \ \ \ \ \ {\isacharbar}\ {\isachardoublequoteopen}replicate\ {\isacharparenleft}Suc\ n{\isacharparenright}\ xs\ {\isacharequal}\ xs\ {\isacharat}\ replicate\ n\ xs{\isachardoublequoteclose}\isanewline
 \isanewline
 \ \ \ \ \isacommand{interpretation}\isamarkupfalse%
-\ list{\isacharunderscore}monoid{\isacharcolon}\ monoid\ {\isacharbrackleft}{\isachardoublequoteopen}op\ {\isacharat}{\isachardoublequoteclose}\ {\isachardoublequoteopen}{\isacharbrackleft}{\isacharbrackright}{\isachardoublequoteclose}{\isacharbrackright}\ \isakeyword{where}\isanewline
-\ \ \ \ \ \ {\isachardoublequoteopen}monoid{\isachardot}pow{\isacharunderscore}nat\ {\isacharparenleft}op\ {\isacharat}{\isacharparenright}\ {\isacharbrackleft}{\isacharbrackright}\ {\isacharequal}\ replicate{\isachardoublequoteclose}\isanewline
+\ list{\isacharunderscore}monoid{\isacharcolon}\ monoid\ {\isacharbrackleft}append\ {\isachardoublequoteopen}{\isacharbrackleft}{\isacharbrackright}{\isachardoublequoteclose}{\isacharbrackright}\ \isakeyword{where}\isanewline
+\ \ \ \ \ \ {\isachardoublequoteopen}monoid{\isachardot}pow{\isacharunderscore}nat\ append\ {\isacharbrackleft}{\isacharbrackright}\ {\isacharequal}\ replicate{\isachardoublequoteclose}\isanewline
 %
 \isadelimproof
 \ \ \ \ %
@@ -821,16 +841,16 @@
 \isacommand{proof}\isamarkupfalse%
 \ {\isacharminus}\isanewline
 \ \ \ \ \ \ \isacommand{interpret}\isamarkupfalse%
-\ monoid\ {\isacharbrackleft}{\isachardoublequoteopen}op\ {\isacharat}{\isachardoublequoteclose}\ {\isachardoublequoteopen}{\isacharbrackleft}{\isacharbrackright}{\isachardoublequoteclose}{\isacharbrackright}\ \isacommand{{\isachardot}{\isachardot}}\isamarkupfalse%
+\ monoid\ {\isacharbrackleft}append\ {\isachardoublequoteopen}{\isacharbrackleft}{\isacharbrackright}{\isachardoublequoteclose}{\isacharbrackright}\ \isacommand{{\isachardot}{\isachardot}}\isamarkupfalse%
 \isanewline
 \ \ \ \ \ \ \isacommand{show}\isamarkupfalse%
-\ {\isachardoublequoteopen}monoid{\isachardot}pow{\isacharunderscore}nat\ {\isacharparenleft}op\ {\isacharat}{\isacharparenright}\ {\isacharbrackleft}{\isacharbrackright}\ {\isacharequal}\ replicate{\isachardoublequoteclose}\isanewline
+\ {\isachardoublequoteopen}monoid{\isachardot}pow{\isacharunderscore}nat\ append\ {\isacharbrackleft}{\isacharbrackright}\ {\isacharequal}\ replicate{\isachardoublequoteclose}\isanewline
 \ \ \ \ \ \ \isacommand{proof}\isamarkupfalse%
 \isanewline
 \ \ \ \ \ \ \ \ \isacommand{fix}\isamarkupfalse%
 \ n\isanewline
 \ \ \ \ \ \ \ \ \isacommand{show}\isamarkupfalse%
-\ {\isachardoublequoteopen}monoid{\isachardot}pow{\isacharunderscore}nat\ {\isacharparenleft}op\ {\isacharat}{\isacharparenright}\ {\isacharbrackleft}{\isacharbrackright}\ n\ {\isacharequal}\ replicate\ n{\isachardoublequoteclose}\isanewline
+\ {\isachardoublequoteopen}monoid{\isachardot}pow{\isacharunderscore}nat\ append\ {\isacharbrackleft}{\isacharbrackright}\ n\ {\isacharequal}\ replicate\ n{\isachardoublequoteclose}\isanewline
 \ \ \ \ \ \ \ \ \ \ \isacommand{by}\isamarkupfalse%
 \ {\isacharparenleft}induct\ n{\isacharparenright}\ auto\isanewline
 \ \ \ \ \ \ \isacommand{qed}\isamarkupfalse%
@@ -932,12 +952,24 @@
   in \isa{group} which uses \isa{pow{\isacharunderscore}nat}:%
 \end{isamarkuptext}%
 \isamarkuptrue%
-\ \ \ \ \isacommand{definition}\isamarkupfalse%
-\ {\isacharparenleft}\isakeyword{in}\ group{\isacharparenright}\isanewline
-\ \ \ \ \ \ pow{\isacharunderscore}int\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequoteopen}int\ {\isasymRightarrow}\ {\isasymalpha}\ {\isasymRightarrow}\ {\isasymalpha}{\isachardoublequoteclose}\ \isakeyword{where}\isanewline
-\ \ \ \ \ \ {\isachardoublequoteopen}pow{\isacharunderscore}int\ k\ x\ {\isacharequal}\ {\isacharparenleft}if\ k\ {\isachargreater}{\isacharequal}\ {\isadigit{0}}\isanewline
-\ \ \ \ \ \ \ \ then\ pow{\isacharunderscore}nat\ {\isacharparenleft}nat\ k{\isacharparenright}\ x\isanewline
-\ \ \ \ \ \ \ \ else\ {\isacharparenleft}pow{\isacharunderscore}nat\ {\isacharparenleft}nat\ {\isacharparenleft}{\isacharminus}\ k{\isacharparenright}{\isacharparenright}\ x{\isacharparenright}{\isasymdiv}{\isacharparenright}{\isachardoublequoteclose}%
+%
+\isadelimquote
+%
+\endisadelimquote
+%
+\isatagquote
+\isacommand{definition}\isamarkupfalse%
+\ {\isacharparenleft}\isakeyword{in}\ group{\isacharparenright}\ pow{\isacharunderscore}int\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequoteopen}int\ {\isasymRightarrow}\ {\isasymalpha}\ {\isasymRightarrow}\ {\isasymalpha}{\isachardoublequoteclose}\ \isakeyword{where}\isanewline
+\ \ {\isachardoublequoteopen}pow{\isacharunderscore}int\ k\ x\ {\isacharequal}\ {\isacharparenleft}if\ k\ {\isachargreater}{\isacharequal}\ {\isadigit{0}}\isanewline
+\ \ \ \ then\ pow{\isacharunderscore}nat\ {\isacharparenleft}nat\ k{\isacharparenright}\ x\isanewline
+\ \ \ \ else\ {\isacharparenleft}pow{\isacharunderscore}nat\ {\isacharparenleft}nat\ {\isacharparenleft}{\isacharminus}\ k{\isacharparenright}{\isacharparenright}\ x{\isacharparenright}{\isasymdiv}{\isacharparenright}{\isachardoublequoteclose}%
+\endisatagquote
+{\isafoldquote}%
+%
+\isadelimquote
+%
+\endisadelimquote
+%
 \begin{isamarkuptext}%
 \noindent yields the global definition of
   \isa{{\isachardoublequote}pow{\isacharunderscore}int\ {\isasymColon}\ int\ {\isasymRightarrow}\ {\isasymalpha}{\isasymColon}group\ {\isasymRightarrow}\ {\isasymalpha}{\isasymColon}group{\isachardoublequote}}
@@ -955,6 +987,12 @@
   uniformly;  type inference resolves ambiguities.  For example:%
 \end{isamarkuptext}%
 \isamarkuptrue%
+%
+\isadelimquote
+%
+\endisadelimquote
+%
+\isatagquote
 \isacommand{context}\isamarkupfalse%
 \ semigroup\isanewline
 \isakeyword{begin}\isanewline
@@ -968,16 +1006,36 @@
 \ {\isachardoublequoteopen}{\isacharparenleft}x{\isasymColon}nat{\isacharparenright}\ {\isasymotimes}\ y{\isachardoublequoteclose}\ %
 \isamarkupcmt{example 2%
 }
+%
+\endisatagquote
+{\isafoldquote}%
+%
+\isadelimquote
+%
+\endisadelimquote
 \isanewline
 \isanewline
 \isacommand{end}\isamarkupfalse%
 \isanewline
+%
+\isadelimquote
 \isanewline
+%
+\endisadelimquote
+%
+\isatagquote
 \isacommand{term}\isamarkupfalse%
 \ {\isachardoublequoteopen}x\ {\isasymotimes}\ y{\isachardoublequoteclose}\ %
 \isamarkupcmt{example 3%
 }
 %
+\endisatagquote
+{\isafoldquote}%
+%
+\isadelimquote
+%
+\endisadelimquote
+%
 \begin{isamarkuptext}%
 \noindent Here in example 1, the term refers to the local class operation
   \isa{mult\ {\isacharbrackleft}{\isasymalpha}{\isacharbrackright}}, whereas in example 2 the type constraint
@@ -994,30 +1052,42 @@
 \begin{isamarkuptext}%
 Turning back to the first motivation for type classes,
   namely overloading, it is obvious that overloading
-  stemming from \isa{{\isasymCLASS}} statements and
-  \isa{{\isasymINSTANTIATION}}
+  stemming from \hyperlink{command.class}{\mbox{\isa{\isacommand{class}}}} statements and
+  \hyperlink{command.instantiation}{\mbox{\isa{\isacommand{instantiation}}}}
   targets naturally maps to Haskell type classes.
   The code generator framework \cite{isabelle-codegen} 
   takes this into account.  Concerning target languages
   lacking type classes (e.g.~SML), type classes
   are implemented by explicit dictionary construction.
-  For example, lets go back to the power function:%
+  As example, let's go back to the power function:%
 \end{isamarkuptext}%
 \isamarkuptrue%
-\ \ \ \ \isacommand{definition}\isamarkupfalse%
-\isanewline
-\ \ \ \ \ \ example\ {\isacharcolon}{\isacharcolon}\ int\ \isakeyword{where}\isanewline
-\ \ \ \ \ \ {\isachardoublequoteopen}example\ {\isacharequal}\ pow{\isacharunderscore}int\ {\isadigit{1}}{\isadigit{0}}\ {\isacharparenleft}{\isacharminus}{\isadigit{2}}{\isacharparenright}{\isachardoublequoteclose}%
+%
+\isadelimquote
+%
+\endisadelimquote
+%
+\isatagquote
+\isacommand{definition}\isamarkupfalse%
+\ example\ {\isacharcolon}{\isacharcolon}\ int\ \isakeyword{where}\isanewline
+\ \ {\isachardoublequoteopen}example\ {\isacharequal}\ pow{\isacharunderscore}int\ {\isadigit{1}}{\isadigit{0}}\ {\isacharparenleft}{\isacharminus}{\isadigit{2}}{\isacharparenright}{\isachardoublequoteclose}%
+\endisatagquote
+{\isafoldquote}%
+%
+\isadelimquote
+%
+\endisadelimquote
+%
 \begin{isamarkuptext}%
 \noindent This maps to Haskell as:%
 \end{isamarkuptext}%
 \isamarkuptrue%
 %
-\isadelimquoteme
+\isadelimquote
 %
-\endisadelimquoteme
+\endisadelimquote
 %
-\isatagquoteme
+\isatagquote
 %
 \begin{isamarkuptext}%
 \isaverbatim%
@@ -1088,23 +1158,23 @@
 \end{isamarkuptext}%
 \isamarkuptrue%
 %
-\endisatagquoteme
-{\isafoldquoteme}%
+\endisatagquote
+{\isafoldquote}%
 %
-\isadelimquoteme
+\isadelimquote
 %
-\endisadelimquoteme
+\endisadelimquote
 %
 \begin{isamarkuptext}%
 \noindent The whole code in SML with explicit dictionary passing:%
 \end{isamarkuptext}%
 \isamarkuptrue%
 %
-\isadelimquoteme
+\isadelimquote
 %
-\endisadelimquoteme
+\endisadelimquote
 %
-\isatagquoteme
+\isatagquote
 %
 \begin{isamarkuptext}%
 \isaverbatim%
@@ -1170,12 +1240,12 @@
 \end{isamarkuptext}%
 \isamarkuptrue%
 %
-\endisatagquoteme
-{\isafoldquoteme}%
+\endisatagquote
+{\isafoldquote}%
 %
-\isadelimquoteme
+\isadelimquote
 %
-\endisadelimquoteme
+\endisadelimquote
 %
 \isadelimtheory
 %
diff -r 1358b1ddd915 -r 519b17118926 doc-src/IsarAdvanced/Classes/classes.tex
--- a/doc-src/IsarAdvanced/Classes/classes.tex	Fri Oct 10 15:23:33 2008 +0200
+++ b/doc-src/IsarAdvanced/Classes/classes.tex	Fri Oct 10 15:52:45 2008 +0200
@@ -3,71 +3,51 @@
 
 \documentclass[12pt,a4paper,fleqn]{report}
 \usepackage{latexsym,graphicx}
-\usepackage{listings}
 \usepackage[refpage]{nomencl}
 \usepackage{../../iman,../../extra,../../isar,../../proof}
 \usepackage{../../isabelle,../../isabellesym}
 \usepackage{style}
 \usepackage{../../pdfsetup}
 
-\newcommand{\isaverbatim}{\renewcommand{\baselinestretch}{1}\setlength{\baselineskip}{8pt}\fontsize{8pt}{0pt}}
-
-\makeatletter
-
-\isakeeptag{quoteme}
-\newenvironment{quoteme}{\begin{quote}\isa@parindent\parindent\parindent0pt\isa@parskip\parskip\parskip0pt}{\end{quote}}
-\renewcommand{\isatagquoteme}{\begin{quoteme}}
-\renewcommand{\endisatagquoteme}{\end{quoteme}}
-
-\makeatother
-
-\renewcommand{\isasymlongleftrightarrow}{\isamath{\leftrightarrow}}
-\renewcommand{\isasymdiv}{\isamath{{}^{-1}}}
-\renewcommand{\isasymotimes}{\isamath{\circ}}
-
-\newcommand{\cmd}[1]{\isacommand{#1}}
 
-\newcommand{\isasymINFIX}{\cmd{infix}}
-\newcommand{\isasymLOCALE}{\cmd{locale}}
-\newcommand{\isasymINCLUDES}{\cmd{includes}}
-\newcommand{\isasymDATATYPE}{\cmd{datatype}}
-\newcommand{\isasymAXCLASS}{\cmd{axclass}}
-\newcommand{\isasymFIXES}{\cmd{fixes}}
-\newcommand{\isasymASSUMES}{\cmd{assumes}}
-\newcommand{\isasymDEFINES}{\cmd{defines}}
-\newcommand{\isasymNOTES}{\cmd{notes}}
-\newcommand{\isasymSHOWS}{\cmd{shows}}
-\newcommand{\isasymCLASS}{\cmd{class}}
-\newcommand{\isasymINSTANCE}{\cmd{instance}}
-\newcommand{\isasymINSTANTIATION}{\cmd{instantiation}}
-\newcommand{\isasymPRINTCONTEXT}{\cmd{print-context}}
-\newcommand{\isasymLEMMA}{\cmd{lemma}}
-\newcommand{\isasymPROOF}{\cmd{proof}}
-\newcommand{\isasymQED}{\cmd{qed}}
-\newcommand{\isasymFIX}{\cmd{fix}}
-\newcommand{\isasymASSUME}{\cmd{assume}}
-\newcommand{\isasymSHOW}{\cmd{show}}
-\newcommand{\isasymNOTE}{\cmd{note}}
+%% setup
 
-\newcommand{\qt}[1]{``#1''}
-\newcommand{\qtt}[1]{"{}{#1}"{}}
-\newcommand{\qn}[1]{\emph{#1}}
-\newcommand{\strong}[1]{{\bfseries #1}}
-\newcommand{\fixme}[1][!]{\strong{FIXME: #1}}
-
-\lstset{basicstyle=\scriptsize\ttfamily,keywordstyle=\itshape,commentstyle=\itshape\sffamily,frame=single}
-\newcommand{\lstsml}[1]{\lstset{language=ML}\lstinputlisting{#1}}
-\newcommand{\lsthaskell}[1]{\lstset{language=Haskell}\lstinputlisting{#1}}
-
+% hyphenation
 \hyphenation{Isabelle}
 \hyphenation{Isar}
 
+% logical markup
+\newcommand{\strong}[1]{{\bfseries {#1}}}
+\newcommand{\qn}[1]{\emph{#1}}
+
+% typographic conventions
+\newcommand{\qt}[1]{``{#1}''}
+
+% verbatim text
+\newcommand{\isaverbatim}{\renewcommand{\baselinestretch}{1}\setlength{\baselineskip}{8pt}\fontsize{8pt}{0pt}}
+
+% invisibility
 \isadroptag{theory}
+
+% quoted segments
+\makeatletter
+\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
+
+%\renewcommand{\isasymlongleftrightarrow}{\isamath{\leftrightarrow}}
+%\renewcommand{\isasymdiv}{\isamath{{}^{-1}}}
+%\renewcommand{\isasymotimes}{\isamath{\circ}}
+
+
+%% content
+
 \title{\includegraphics[scale=0.5]{isabelle_isar}
   \\[4ex] Haskell-style type classes with Isabelle/Isar}
 \author{\emph{Florian Haftmann}}
 
-
 \begin{document}
 
 \maketitle