tuned

--- a/doc-src/IsarAdvanced/Classes/Thy/Classes.thy	Fri Oct 10 15:52:45 2008 +0200
+++ b/doc-src/IsarAdvanced/Classes/Thy/Classes.thy	Fri Oct 10 16:02:15 2008 +0200
@@ -141,7 +141,7 @@
 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 .
+    unfolding mult_int_def .
 qed
 
 end %quote
@@ -207,7 +207,7 @@
 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)
+    unfolding mult_prod_def by (simp add: assoc)
 qed      
 
 end %quote
@@ -244,98 +244,99 @@
   for types with the same arity may be simultaneous:
 *}
 
-    instantiation nat and int :: monoidl
-    begin
+instantiation %quote nat and int :: monoidl
+begin
 
-    definition
-      neutral_nat_def: "\<one> = (0\<Colon>nat)"
+definition %quote
+  neutral_nat_def: "\<one> = (0\<Colon>nat)"
 
-    definition
-      neutral_int_def: "\<one> = (0\<Colon>int)"
+definition %quote
+  neutral_int_def: "\<one> = (0\<Colon>int)"
 
-    instance proof
-      fix n :: nat
-      show "\<one> \<otimes> n = n"
-	unfolding neutral_nat_def by simp
-    next
-      fix k :: int
-      show "\<one> \<otimes> k = k"
-	unfolding neutral_int_def mult_int_def by simp
-    qed
+instance %quote proof
+  fix n :: nat
+  show "\<one> \<otimes> n = n"
+    unfolding neutral_nat_def by simp
+next
+  fix k :: int
+  show "\<one> \<otimes> k = k"
+    unfolding neutral_int_def mult_int_def by simp
+qed
 
-    end
+end %quote
 
-    instantiation * :: (monoidl, monoidl) monoidl
-    begin
+instantiation %quote * :: (monoidl, monoidl) monoidl
+begin
 
-    definition
-      neutral_prod_def: "\<one> = (\<one>, \<one>)"
+definition %quote
+  neutral_prod_def: "\<one> = (\<one>, \<one>)"
 
-    instance proof
-      fix p :: "\<alpha>\<Colon>monoidl \<times> \<beta>\<Colon>monoidl"
-      show "\<one> \<otimes> p = p"
-	unfolding neutral_prod_def mult_prod_def by (simp add: neutl)
-    qed
+instance %quote proof
+  fix p :: "\<alpha>\<Colon>monoidl \<times> \<beta>\<Colon>monoidl"
+  show "\<one> \<otimes> p = p"
+    unfolding neutral_prod_def mult_prod_def by (simp add: neutl)
+qed
 
-   end
+end %quote
 
 text {*
   \noindent Fully-fledged monoids are modelled by another subclass
   which does not add new parameters but tightens the specification:
 *}
 
-    class monoid = monoidl +
-      assumes neutr: "x \<otimes> \<one> = x"
+class %quote monoid = monoidl +
+  assumes neutr: "x \<otimes> \<one> = x"
 
-    instantiation nat and int :: monoid 
-    begin
+instantiation %quote nat and int :: monoid 
+begin
 
-    instance proof
-      fix n :: nat
-      show "n \<otimes> \<one> = n"
-	unfolding neutral_nat_def by (induct n) simp_all
-    next
-      fix k :: int
-      show "k \<otimes> \<one> = k"
-	unfolding neutral_int_def mult_int_def by simp
-    qed
+instance %quote proof
+  fix n :: nat
+  show "n \<otimes> \<one> = n"
+    unfolding neutral_nat_def by (induct n) simp_all
+next
+  fix k :: int
+  show "k \<otimes> \<one> = k"
+    unfolding neutral_int_def mult_int_def by simp
+qed
 
-    end
+end %quote
 
-    instantiation * :: (monoid, monoid) monoid
-    begin
+instantiation %quote * :: (monoid, monoid) monoid
+begin
 
-    instance proof 
-      fix p :: "\<alpha>\<Colon>monoid \<times> \<beta>\<Colon>monoid"
-      show "p \<otimes> \<one> = p"
-	unfolding neutral_prod_def mult_prod_def by (simp add: neutr)
-    qed
+instance %quote proof 
+  fix p :: "\<alpha>\<Colon>monoid \<times> \<beta>\<Colon>monoid"
+  show "p \<otimes> \<one> = p"
+    unfolding neutral_prod_def mult_prod_def by (simp add: neutr)
+qed
 
-    end
+end %quote
 
 text {*
   \noindent To finish our small algebra example, we add a @{text group} class
   with a corresponding instance:
 *}
 
-    class group = monoidl +
-      fixes inverse :: "\<alpha> \<Rightarrow> \<alpha>"    ("(_\<div>)" [1000] 999)
-      assumes invl: "x\<div> \<otimes> x = \<one>"
+class %quote group = monoidl +
+  fixes inverse :: "\<alpha> \<Rightarrow> \<alpha>"    ("(_\<div>)" [1000] 999)
+  assumes invl: "x\<div> \<otimes> x = \<one>"
 
-    instantiation int :: group
-    begin
+instantiation %quote int :: group
+begin
+
+definition %quote
+  inverse_int_def: "i\<div> = - (i\<Colon>int)"
 
-    definition
-      inverse_int_def: "i\<div> = - (i\<Colon>int)"
+instance %quote proof
+  fix i :: int
+  have "-i + i = 0" by simp
+  then show "i\<div> \<otimes> i = \<one>"
+    unfolding mult_int_def neutral_int_def inverse_int_def .
+qed
 
-    instance proof
-      fix i :: int
-      have "-i + i = 0" by simp
-      then show "i\<div> \<otimes> i = \<one>"
-	unfolding mult_int_def neutral_int_def inverse_int_def .
-    qed
+end %quote
 
-    end
 
 section {* Type classes as locales *}
 
@@ -348,45 +349,41 @@
   is nothing else than a locale:
 *}
 
-class idem = type +
+class %quote idem = type +
   fixes f :: "\<alpha> \<Rightarrow> \<alpha>"
   assumes idem: "f (f x) = f x"
 
 text {*
   \noindent essentially introduces the locale
-*}
+*} setup %invisible {* Sign.add_path "foo" *}
 
-setup %invisible {* Sign.add_path "foo" *}
-
-locale idem =
+locale %quote idem =
   fixes f :: "\<alpha> \<Rightarrow> \<alpha>"
   assumes idem: "f (f x) = f x"
 
 text {* \noindent together with corresponding constant(s): *}
 
-consts f :: "\<alpha> \<Rightarrow> \<alpha>"
+consts %quote f :: "\<alpha> \<Rightarrow> \<alpha>"
 
 text {*
   \noindent The connection to the type system is done by means
   of a primitive axclass
 *}
 
-axclass idem < type
+axclass %quote idem < type
   idem: "f (f x) = f x"
 
 text {* \noindent together with a corresponding interpretation: *}
 
-interpretation idem_class:
+interpretation %quote idem_class:
   idem ["f \<Colon> (\<alpha>\<Colon>idem) \<Rightarrow> \<alpha>"]
 by unfold_locales (rule idem)
 
-setup %invisible {* Sign.parent_path *}
-
 text {*
-  This give you at hand the full power of the Isabelle module system;
+  \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 *}
 
 subsection {* Abstract reasoning *}
 
@@ -397,16 +394,16 @@
   states that the function @{text "(x \<otimes>)"} is injective:
 *}
 
-    lemma (in group) left_cancel: "x \<otimes> y = x \<otimes> z \<longleftrightarrow> y = z"
-    proof
-      assume "x \<otimes> y = x \<otimes> z"
-      then have "x\<div> \<otimes> (x \<otimes> y) = x\<div> \<otimes> (x \<otimes> z)" by simp
-      then have "(x\<div> \<otimes> x) \<otimes> y = (x\<div> \<otimes> x) \<otimes> z" using assoc by simp
-      then show "y = z" using neutl and invl by simp
-    next
-      assume "y = z"
-      then show "x \<otimes> y = x \<otimes> z" by simp
-    qed
+lemma %quote (in group) left_cancel: "x \<otimes> y = x \<otimes> z \<longleftrightarrow> y = z"
+proof
+  assume "x \<otimes> y = x \<otimes> z"
+  then have "x\<div> \<otimes> (x \<otimes> y) = x\<div> \<otimes> (x \<otimes> z)" by simp
+  then have "(x\<div> \<otimes> x) \<otimes> y = (x\<div> \<otimes> x) \<otimes> z" using assoc by simp
+  then show "y = z" using neutl and invl by simp
+next
+  assume "y = z"
+  then show "x \<otimes> y = x \<otimes> z" by simp
+qed
 
 text {*
   \noindent Here the \qt{@{keyword "in"} @{class group}} target specification
@@ -426,9 +423,9 @@
   in locales:
 *}
 
-    primrec (in monoid) pow_nat :: "nat \<Rightarrow> \<alpha> \<Rightarrow> \<alpha>" where
-      "pow_nat 0 x = \<one>"
-      | "pow_nat (Suc n) x = x \<otimes> pow_nat n x"
+primrec %quote (in monoid) pow_nat :: "nat \<Rightarrow> \<alpha> \<Rightarrow> \<alpha>" where
+  "pow_nat 0 x = \<one>"
+  | "pow_nat (Suc n) x = x \<otimes> pow_nat n x"
 
 text {*
   \noindent If the locale @{text group} is also a class, this local
@@ -462,8 +459,8 @@
   of monoids for lists:
 *}
 
-    interpretation list_monoid: monoid [append "[]"]
-      by unfold_locales auto
+interpretation %quote list_monoid: monoid [append "[]"]
+  by unfold_locales auto
 
 text {*
   \noindent This enables us to apply facts on monoids
@@ -473,21 +470,21 @@
   be appropriate to map derived definitions accordingly:
 *}
 
-    fun replicate :: "nat \<Rightarrow> \<alpha> list \<Rightarrow> \<alpha> list" where
-      "replicate 0 _ = []"
-      | "replicate (Suc n) xs = xs @ replicate n xs"
+primrec %quote replicate :: "nat \<Rightarrow> \<alpha> list \<Rightarrow> \<alpha> list" where
+  "replicate 0 _ = []"
+  | "replicate (Suc n) xs = xs @ replicate n xs"
 
-    interpretation list_monoid: monoid [append "[]"] where
-      "monoid.pow_nat append [] = replicate"
-    proof -
-      interpret monoid [append "[]"] ..
-      show "monoid.pow_nat append [] = replicate"
-      proof
-        fix n
-        show "monoid.pow_nat append [] n = replicate n"
-          by (induct n) auto
-      qed
-    qed intro_locales
+interpretation %quote list_monoid: monoid [append "[]"] where
+  "monoid.pow_nat append [] = replicate"
+proof -
+  interpret monoid [append "[]"] ..
+  show "monoid.pow_nat append [] = replicate"
+  proof
+    fix n
+    show "monoid.pow_nat append [] n = replicate n"
+      by (induct n) auto
+  qed
+qed intro_locales
 
 
 subsection {* Additional subclass relations *}
@@ -499,13 +496,13 @@
   together with a proof of the logical difference:
 *}
 
-    subclass (in group) monoid
-    proof unfold_locales
-      fix x
-      from invl have "x\<div> \<otimes> x = \<one>" by simp
-      with assoc [symmetric] neutl invl have "x\<div> \<otimes> (x \<otimes> \<one>) = x\<div> \<otimes> x" by simp
-      with left_cancel show "x \<otimes> \<one> = x" by simp
-    qed
+subclass %quote (in group) monoid
+proof unfold_locales
+  fix x
+  from invl have "x\<div> \<otimes> x = \<one>" by simp
+  with assoc [symmetric] neutl invl have "x\<div> \<otimes> (x \<otimes> \<one>) = x\<div> \<otimes> x" by simp
+  with left_cancel show "x \<otimes> \<one> = x" by simp
+qed
 
 text {*
   \noindent The logical proof is carried out on the locale level
@@ -576,7 +573,7 @@
 term %quote "x \<otimes> y" -- {* example 1 *}
 term %quote "(x\<Colon>nat) \<otimes> y" -- {* example 2 *}
 
-end
+end  %quote
 
 term %quote "x \<otimes> y" -- {* example 3 *}
 

--- a/doc-src/IsarAdvanced/Classes/Thy/document/Classes.tex	Fri Oct 10 15:52:45 2008 +0200
+++ b/doc-src/IsarAdvanced/Classes/Thy/document/Classes.tex	Fri Oct 10 16:02:15 2008 +0200
@@ -194,7 +194,7 @@
 \ \ \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%
@@ -306,7 +306,7 @@
 \ 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%
 \ {\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%
@@ -368,224 +368,198 @@
   for types with the same arity may be simultaneous:%
 \end{isamarkuptext}%
 \isamarkuptrue%
-\ \ \ \ \isacommand{instantiation}\isamarkupfalse%
+%
+\isadelimquote
+%
+\endisadelimquote
+%
+\isatagquote
+\isacommand{instantiation}\isamarkupfalse%
 \ nat\ \isakeyword{and}\ int\ {\isacharcolon}{\isacharcolon}\ monoidl\isanewline
-\ \ \ \ \isakeyword{begin}\isanewline
-\isanewline
-\ \ \ \ \isacommand{definition}\isamarkupfalse%
+\isakeyword{begin}\isanewline
 \isanewline
-\ \ \ \ \ \ neutral{\isacharunderscore}nat{\isacharunderscore}def{\isacharcolon}\ {\isachardoublequoteopen}{\isasymone}\ {\isacharequal}\ {\isacharparenleft}{\isadigit{0}}{\isasymColon}nat{\isacharparenright}{\isachardoublequoteclose}\isanewline
-\isanewline
-\ \ \ \ \isacommand{definition}\isamarkupfalse%
-\isanewline
-\ \ \ \ \ \ neutral{\isacharunderscore}int{\isacharunderscore}def{\isacharcolon}\ {\isachardoublequoteopen}{\isasymone}\ {\isacharequal}\ {\isacharparenleft}{\isadigit{0}}{\isasymColon}int{\isacharparenright}{\isachardoublequoteclose}\isanewline
+\isacommand{definition}\isamarkupfalse%
 \isanewline
-\ \ \ \ \isacommand{instance}\isamarkupfalse%
-%
-\isadelimproof
-\ %
-\endisadelimproof
-%
-\isatagproof
-\isacommand{proof}\isamarkupfalse%
+\ \ neutral{\isacharunderscore}nat{\isacharunderscore}def{\isacharcolon}\ {\isachardoublequoteopen}{\isasymone}\ {\isacharequal}\ {\isacharparenleft}{\isadigit{0}}{\isasymColon}nat{\isacharparenright}{\isachardoublequoteclose}\isanewline
+\isanewline
+\isacommand{definition}\isamarkupfalse%
+\isanewline
+\ \ neutral{\isacharunderscore}int{\isacharunderscore}def{\isacharcolon}\ {\isachardoublequoteopen}{\isasymone}\ {\isacharequal}\ {\isacharparenleft}{\isadigit{0}}{\isasymColon}int{\isacharparenright}{\isachardoublequoteclose}\isanewline
 \isanewline
-\ \ \ \ \ \ \isacommand{fix}\isamarkupfalse%
+\isacommand{instance}\isamarkupfalse%
+\ \isacommand{proof}\isamarkupfalse%
+\isanewline
+\ \ \isacommand{fix}\isamarkupfalse%
 \ n\ {\isacharcolon}{\isacharcolon}\ nat\isanewline
-\ \ \ \ \ \ \isacommand{show}\isamarkupfalse%
+\ \ \isacommand{show}\isamarkupfalse%
 \ {\isachardoublequoteopen}{\isasymone}\ {\isasymotimes}\ n\ {\isacharequal}\ n{\isachardoublequoteclose}\isanewline
-\ \ \ \ \ \ \ \ \isacommand{unfolding}\isamarkupfalse%
+\ \ \ \ \isacommand{unfolding}\isamarkupfalse%
 \ neutral{\isacharunderscore}nat{\isacharunderscore}def\ \isacommand{by}\isamarkupfalse%
 \ simp\isanewline
-\ \ \ \ \isacommand{next}\isamarkupfalse%
+\isacommand{next}\isamarkupfalse%
 \isanewline
-\ \ \ \ \ \ \isacommand{fix}\isamarkupfalse%
+\ \ \isacommand{fix}\isamarkupfalse%
 \ k\ {\isacharcolon}{\isacharcolon}\ int\isanewline
-\ \ \ \ \ \ \isacommand{show}\isamarkupfalse%
+\ \ \isacommand{show}\isamarkupfalse%
 \ {\isachardoublequoteopen}{\isasymone}\ {\isasymotimes}\ k\ {\isacharequal}\ k{\isachardoublequoteclose}\isanewline
-\ \ \ \ \ \ \ \ \isacommand{unfolding}\isamarkupfalse%
+\ \ \ \ \isacommand{unfolding}\isamarkupfalse%
 \ neutral{\isacharunderscore}int{\isacharunderscore}def\ mult{\isacharunderscore}int{\isacharunderscore}def\ \isacommand{by}\isamarkupfalse%
 \ simp\isanewline
-\ \ \ \ \isacommand{qed}\isamarkupfalse%
-%
-\endisatagproof
-{\isafoldproof}%
-%
-\isadelimproof
-%
-\endisadelimproof
+\isacommand{qed}\isamarkupfalse%
 \isanewline
 \isanewline
-\ \ \ \ \isacommand{end}\isamarkupfalse%
+\isacommand{end}\isamarkupfalse%
 \isanewline
 \isanewline
-\ \ \ \ \isacommand{instantiation}\isamarkupfalse%
+\isacommand{instantiation}\isamarkupfalse%
 \ {\isacharasterisk}\ {\isacharcolon}{\isacharcolon}\ {\isacharparenleft}monoidl{\isacharcomma}\ monoidl{\isacharparenright}\ monoidl\isanewline
-\ \ \ \ \isakeyword{begin}\isanewline
+\isakeyword{begin}\isanewline
 \isanewline
-\ \ \ \ \isacommand{definition}\isamarkupfalse%
+\isacommand{definition}\isamarkupfalse%
 \isanewline
-\ \ \ \ \ \ neutral{\isacharunderscore}prod{\isacharunderscore}def{\isacharcolon}\ {\isachardoublequoteopen}{\isasymone}\ {\isacharequal}\ {\isacharparenleft}{\isasymone}{\isacharcomma}\ {\isasymone}{\isacharparenright}{\isachardoublequoteclose}\isanewline
+\ \ neutral{\isacharunderscore}prod{\isacharunderscore}def{\isacharcolon}\ {\isachardoublequoteopen}{\isasymone}\ {\isacharequal}\ {\isacharparenleft}{\isasymone}{\isacharcomma}\ {\isasymone}{\isacharparenright}{\isachardoublequoteclose}\isanewline
 \isanewline
-\ \ \ \ \isacommand{instance}\isamarkupfalse%
-%
-\isadelimproof
-\ %
-\endisadelimproof
-%
-\isatagproof
-\isacommand{proof}\isamarkupfalse%
+\isacommand{instance}\isamarkupfalse%
+\ \isacommand{proof}\isamarkupfalse%
 \isanewline
-\ \ \ \ \ \ \isacommand{fix}\isamarkupfalse%
+\ \ \isacommand{fix}\isamarkupfalse%
 \ p\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequoteopen}{\isasymalpha}{\isasymColon}monoidl\ {\isasymtimes}\ {\isasymbeta}{\isasymColon}monoidl{\isachardoublequoteclose}\isanewline
-\ \ \ \ \ \ \isacommand{show}\isamarkupfalse%
+\ \ \isacommand{show}\isamarkupfalse%
 \ {\isachardoublequoteopen}{\isasymone}\ {\isasymotimes}\ p\ {\isacharequal}\ p{\isachardoublequoteclose}\isanewline
-\ \ \ \ \ \ \ \ \isacommand{unfolding}\isamarkupfalse%
+\ \ \ \ \isacommand{unfolding}\isamarkupfalse%
 \ neutral{\isacharunderscore}prod{\isacharunderscore}def\ mult{\isacharunderscore}prod{\isacharunderscore}def\ \isacommand{by}\isamarkupfalse%
 \ {\isacharparenleft}simp\ add{\isacharcolon}\ neutl{\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 Fully-fledged monoids are modelled by another subclass
   which does not add new parameters but tightens the specification:%
 \end{isamarkuptext}%
 \isamarkuptrue%
-\ \ \ \ \isacommand{class}\isamarkupfalse%
-\ monoid\ {\isacharequal}\ monoidl\ {\isacharplus}\isanewline
-\ \ \ \ \ \ \isakeyword{assumes}\ neutr{\isacharcolon}\ {\isachardoublequoteopen}x\ {\isasymotimes}\ {\isasymone}\ {\isacharequal}\ x{\isachardoublequoteclose}\isanewline
-\isanewline
-\ \ \ \ \isacommand{instantiation}\isamarkupfalse%
-\ nat\ \isakeyword{and}\ int\ {\isacharcolon}{\isacharcolon}\ monoid\ \isanewline
-\ \ \ \ \isakeyword{begin}\isanewline
-\isanewline
-\ \ \ \ \isacommand{instance}\isamarkupfalse%
+%
+\isadelimquote
+%
+\endisadelimquote
 %
-\isadelimproof
-\ %
-\endisadelimproof
-%
-\isatagproof
-\isacommand{proof}\isamarkupfalse%
+\isatagquote
+\isacommand{class}\isamarkupfalse%
+\ monoid\ {\isacharequal}\ monoidl\ {\isacharplus}\isanewline
+\ \ \isakeyword{assumes}\ neutr{\isacharcolon}\ {\isachardoublequoteopen}x\ {\isasymotimes}\ {\isasymone}\ {\isacharequal}\ x{\isachardoublequoteclose}\isanewline
+\isanewline
+\isacommand{instantiation}\isamarkupfalse%
+\ nat\ \isakeyword{and}\ int\ {\isacharcolon}{\isacharcolon}\ monoid\ \isanewline
+\isakeyword{begin}\isanewline
 \isanewline
-\ \ \ \ \ \ \isacommand{fix}\isamarkupfalse%
+\isacommand{instance}\isamarkupfalse%
+\ \isacommand{proof}\isamarkupfalse%
+\isanewline
+\ \ \isacommand{fix}\isamarkupfalse%
 \ n\ {\isacharcolon}{\isacharcolon}\ nat\isanewline
-\ \ \ \ \ \ \isacommand{show}\isamarkupfalse%
+\ \ \isacommand{show}\isamarkupfalse%
 \ {\isachardoublequoteopen}n\ {\isasymotimes}\ {\isasymone}\ {\isacharequal}\ n{\isachardoublequoteclose}\isanewline
-\ \ \ \ \ \ \ \ \isacommand{unfolding}\isamarkupfalse%
+\ \ \ \ \isacommand{unfolding}\isamarkupfalse%
 \ neutral{\isacharunderscore}nat{\isacharunderscore}def\ \isacommand{by}\isamarkupfalse%
 \ {\isacharparenleft}induct\ n{\isacharparenright}\ simp{\isacharunderscore}all\isanewline
-\ \ \ \ \isacommand{next}\isamarkupfalse%
+\isacommand{next}\isamarkupfalse%
 \isanewline
-\ \ \ \ \ \ \isacommand{fix}\isamarkupfalse%
+\ \ \isacommand{fix}\isamarkupfalse%
 \ k\ {\isacharcolon}{\isacharcolon}\ int\isanewline
-\ \ \ \ \ \ \isacommand{show}\isamarkupfalse%
+\ \ \isacommand{show}\isamarkupfalse%
 \ {\isachardoublequoteopen}k\ {\isasymotimes}\ {\isasymone}\ {\isacharequal}\ k{\isachardoublequoteclose}\isanewline
-\ \ \ \ \ \ \ \ \isacommand{unfolding}\isamarkupfalse%
+\ \ \ \ \isacommand{unfolding}\isamarkupfalse%
 \ neutral{\isacharunderscore}int{\isacharunderscore}def\ mult{\isacharunderscore}int{\isacharunderscore}def\ \isacommand{by}\isamarkupfalse%
 \ simp\isanewline
-\ \ \ \ \isacommand{qed}\isamarkupfalse%
-%
-\endisatagproof
-{\isafoldproof}%
-%
-\isadelimproof
-%
-\endisadelimproof
+\isacommand{qed}\isamarkupfalse%
 \isanewline
 \isanewline
-\ \ \ \ \isacommand{end}\isamarkupfalse%
+\isacommand{end}\isamarkupfalse%
 \isanewline
 \isanewline
-\ \ \ \ \isacommand{instantiation}\isamarkupfalse%
+\isacommand{instantiation}\isamarkupfalse%
 \ {\isacharasterisk}\ {\isacharcolon}{\isacharcolon}\ {\isacharparenleft}monoid{\isacharcomma}\ monoid{\isacharparenright}\ monoid\isanewline
-\ \ \ \ \isakeyword{begin}\isanewline
+\isakeyword{begin}\isanewline
 \isanewline
-\ \ \ \ \isacommand{instance}\isamarkupfalse%
-%
-\isadelimproof
-\ %
-\endisadelimproof
-%
-\isatagproof
-\isacommand{proof}\isamarkupfalse%
+\isacommand{instance}\isamarkupfalse%
+\ \isacommand{proof}\isamarkupfalse%
 \ \isanewline
-\ \ \ \ \ \ \isacommand{fix}\isamarkupfalse%
+\ \ \isacommand{fix}\isamarkupfalse%
 \ p\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequoteopen}{\isasymalpha}{\isasymColon}monoid\ {\isasymtimes}\ {\isasymbeta}{\isasymColon}monoid{\isachardoublequoteclose}\isanewline
-\ \ \ \ \ \ \isacommand{show}\isamarkupfalse%
+\ \ \isacommand{show}\isamarkupfalse%
 \ {\isachardoublequoteopen}p\ {\isasymotimes}\ {\isasymone}\ {\isacharequal}\ p{\isachardoublequoteclose}\isanewline
-\ \ \ \ \ \ \ \ \isacommand{unfolding}\isamarkupfalse%
+\ \ \ \ \isacommand{unfolding}\isamarkupfalse%
 \ neutral{\isacharunderscore}prod{\isacharunderscore}def\ mult{\isacharunderscore}prod{\isacharunderscore}def\ \isacommand{by}\isamarkupfalse%
 \ {\isacharparenleft}simp\ add{\isacharcolon}\ neutr{\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 To finish our small algebra example, we add a \isa{group} class
   with a corresponding instance:%
 \end{isamarkuptext}%
 \isamarkuptrue%
-\ \ \ \ \isacommand{class}\isamarkupfalse%
+%
+\isadelimquote
+%
+\endisadelimquote
+%
+\isatagquote
+\isacommand{class}\isamarkupfalse%
 \ group\ {\isacharequal}\ monoidl\ {\isacharplus}\isanewline
-\ \ \ \ \ \ \isakeyword{fixes}\ inverse\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequoteopen}{\isasymalpha}\ {\isasymRightarrow}\ {\isasymalpha}{\isachardoublequoteclose}\ \ \ \ {\isacharparenleft}{\isachardoublequoteopen}{\isacharparenleft}{\isacharunderscore}{\isasymdiv}{\isacharparenright}{\isachardoublequoteclose}\ {\isacharbrackleft}{\isadigit{1}}{\isadigit{0}}{\isadigit{0}}{\isadigit{0}}{\isacharbrackright}\ {\isadigit{9}}{\isadigit{9}}{\isadigit{9}}{\isacharparenright}\isanewline
-\ \ \ \ \ \ \isakeyword{assumes}\ invl{\isacharcolon}\ {\isachardoublequoteopen}x{\isasymdiv}\ {\isasymotimes}\ x\ {\isacharequal}\ {\isasymone}{\isachardoublequoteclose}\isanewline
-\isanewline
-\ \ \ \ \isacommand{instantiation}\isamarkupfalse%
-\ int\ {\isacharcolon}{\isacharcolon}\ group\isanewline
-\ \ \ \ \isakeyword{begin}\isanewline
-\isanewline
-\ \ \ \ \isacommand{definition}\isamarkupfalse%
-\isanewline
-\ \ \ \ \ \ inverse{\isacharunderscore}int{\isacharunderscore}def{\isacharcolon}\ {\isachardoublequoteopen}i{\isasymdiv}\ {\isacharequal}\ {\isacharminus}\ {\isacharparenleft}i{\isasymColon}int{\isacharparenright}{\isachardoublequoteclose}\isanewline
+\ \ \isakeyword{fixes}\ inverse\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequoteopen}{\isasymalpha}\ {\isasymRightarrow}\ {\isasymalpha}{\isachardoublequoteclose}\ \ \ \ {\isacharparenleft}{\isachardoublequoteopen}{\isacharparenleft}{\isacharunderscore}{\isasymdiv}{\isacharparenright}{\isachardoublequoteclose}\ {\isacharbrackleft}{\isadigit{1}}{\isadigit{0}}{\isadigit{0}}{\isadigit{0}}{\isacharbrackright}\ {\isadigit{9}}{\isadigit{9}}{\isadigit{9}}{\isacharparenright}\isanewline
+\ \ \isakeyword{assumes}\ invl{\isacharcolon}\ {\isachardoublequoteopen}x{\isasymdiv}\ {\isasymotimes}\ x\ {\isacharequal}\ {\isasymone}{\isachardoublequoteclose}\isanewline
 \isanewline
-\ \ \ \ \isacommand{instance}\isamarkupfalse%
-%
-\isadelimproof
-\ %
-\endisadelimproof
-%
-\isatagproof
-\isacommand{proof}\isamarkupfalse%
+\isacommand{instantiation}\isamarkupfalse%
+\ int\ {\isacharcolon}{\isacharcolon}\ group\isanewline
+\isakeyword{begin}\isanewline
+\isanewline
+\isacommand{definition}\isamarkupfalse%
 \isanewline
-\ \ \ \ \ \ \isacommand{fix}\isamarkupfalse%
+\ \ inverse{\isacharunderscore}int{\isacharunderscore}def{\isacharcolon}\ {\isachardoublequoteopen}i{\isasymdiv}\ {\isacharequal}\ {\isacharminus}\ {\isacharparenleft}i{\isasymColon}int{\isacharparenright}{\isachardoublequoteclose}\isanewline
+\isanewline
+\isacommand{instance}\isamarkupfalse%
+\ \isacommand{proof}\isamarkupfalse%
+\isanewline
+\ \ \isacommand{fix}\isamarkupfalse%
 \ i\ {\isacharcolon}{\isacharcolon}\ int\isanewline
-\ \ \ \ \ \ \isacommand{have}\isamarkupfalse%
+\ \ \isacommand{have}\isamarkupfalse%
 \ {\isachardoublequoteopen}{\isacharminus}i\ {\isacharplus}\ i\ {\isacharequal}\ {\isadigit{0}}{\isachardoublequoteclose}\ \isacommand{by}\isamarkupfalse%
 \ simp\isanewline
-\ \ \ \ \ \ \isacommand{then}\isamarkupfalse%
+\ \ \isacommand{then}\isamarkupfalse%
 \ \isacommand{show}\isamarkupfalse%
 \ {\isachardoublequoteopen}i{\isasymdiv}\ {\isasymotimes}\ i\ {\isacharequal}\ {\isasymone}{\isachardoublequoteclose}\isanewline
-\ \ \ \ \ \ \ \ \isacommand{unfolding}\isamarkupfalse%
+\ \ \ \ \isacommand{unfolding}\isamarkupfalse%
 \ mult{\isacharunderscore}int{\isacharunderscore}def\ neutral{\isacharunderscore}int{\isacharunderscore}def\ inverse{\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
 %
 \isamarkupsection{Type classes as locales%
 }
@@ -602,17 +576,30 @@
   is nothing else than a locale:%
 \end{isamarkuptext}%
 \isamarkuptrue%
+%
+\isadelimquote
+%
+\endisadelimquote
+%
+\isatagquote
 \isacommand{class}\isamarkupfalse%
 \ idem\ {\isacharequal}\ type\ {\isacharplus}\isanewline
 \ \ \isakeyword{fixes}\ f\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequoteopen}{\isasymalpha}\ {\isasymRightarrow}\ {\isasymalpha}{\isachardoublequoteclose}\isanewline
 \ \ \isakeyword{assumes}\ idem{\isacharcolon}\ {\isachardoublequoteopen}f\ {\isacharparenleft}f\ x{\isacharparenright}\ {\isacharequal}\ f\ x{\isachardoublequoteclose}%
+\endisatagquote
+{\isafoldquote}%
+%
+\isadelimquote
+%
+\endisadelimquote
+%
 \begin{isamarkuptext}%
 \noindent essentially introduces the locale%
 \end{isamarkuptext}%
 \isamarkuptrue%
 %
 \isadeliminvisible
-%
+\ %
 \endisadeliminvisible
 %
 \isataginvisible
@@ -625,51 +612,95 @@
 %
 \endisadeliminvisible
 \isanewline
+%
+\isadelimquote
 \isanewline
+%
+\endisadelimquote
+%
+\isatagquote
 \isacommand{locale}\isamarkupfalse%
 \ idem\ {\isacharequal}\isanewline
 \ \ \isakeyword{fixes}\ f\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequoteopen}{\isasymalpha}\ {\isasymRightarrow}\ {\isasymalpha}{\isachardoublequoteclose}\isanewline
 \ \ \isakeyword{assumes}\ idem{\isacharcolon}\ {\isachardoublequoteopen}f\ {\isacharparenleft}f\ x{\isacharparenright}\ {\isacharequal}\ f\ x{\isachardoublequoteclose}%
+\endisatagquote
+{\isafoldquote}%
+%
+\isadelimquote
+%
+\endisadelimquote
+%
 \begin{isamarkuptext}%
 \noindent together with corresponding constant(s):%
 \end{isamarkuptext}%
 \isamarkuptrue%
+%
+\isadelimquote
+%
+\endisadelimquote
+%
+\isatagquote
 \isacommand{consts}\isamarkupfalse%
 \ f\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequoteopen}{\isasymalpha}\ {\isasymRightarrow}\ {\isasymalpha}{\isachardoublequoteclose}%
+\endisatagquote
+{\isafoldquote}%
+%
+\isadelimquote
+%
+\endisadelimquote
+%
 \begin{isamarkuptext}%
 \noindent The connection to the type system is done by means
   of a primitive axclass%
 \end{isamarkuptext}%
 \isamarkuptrue%
+%
+\isadelimquote
+%
+\endisadelimquote
+%
+\isatagquote
 \isacommand{axclass}\isamarkupfalse%
 \ idem\ {\isacharless}\ type\isanewline
 \ \ idem{\isacharcolon}\ {\isachardoublequoteopen}f\ {\isacharparenleft}f\ x{\isacharparenright}\ {\isacharequal}\ f\ x{\isachardoublequoteclose}%
+\endisatagquote
+{\isafoldquote}%
+%
+\isadelimquote
+%
+\endisadelimquote
+%
 \begin{isamarkuptext}%
 \noindent together with a corresponding interpretation:%
 \end{isamarkuptext}%
 \isamarkuptrue%
+%
+\isadelimquote
+%
+\endisadelimquote
+%
+\isatagquote
 \isacommand{interpretation}\isamarkupfalse%
 \ idem{\isacharunderscore}class{\isacharcolon}\isanewline
 \ \ idem\ {\isacharbrackleft}{\isachardoublequoteopen}f\ {\isasymColon}\ {\isacharparenleft}{\isasymalpha}{\isasymColon}idem{\isacharparenright}\ {\isasymRightarrow}\ {\isasymalpha}{\isachardoublequoteclose}{\isacharbrackright}\isanewline
-%
-\isadelimproof
-%
-\endisadelimproof
-%
-\isatagproof
 \isacommand{by}\isamarkupfalse%
 \ unfold{\isacharunderscore}locales\ {\isacharparenleft}rule\ idem{\isacharparenright}%
-\endisatagproof
-{\isafoldproof}%
+\endisatagquote
+{\isafoldquote}%
+%
+\isadelimquote
+%
+\endisadelimquote
 %
-\isadelimproof
-\isanewline
-%
-\endisadelimproof
+\begin{isamarkuptext}%
+\noindent This gives you at hand the full power of the Isabelle module system;
+  conclusions in locale \isa{idem} are implicitly propagated
+  to class \isa{idem}.%
+\end{isamarkuptext}%
+\isamarkuptrue%
 %
 \isadeliminvisible
-\isanewline
-%
+\ %
 \endisadeliminvisible
 %
 \isataginvisible
@@ -682,13 +713,6 @@
 %
 \endisadeliminvisible
 %
-\begin{isamarkuptext}%
-This give you at hand the full power of the Isabelle module system;
-  conclusions in locale \isa{idem} are implicitly propagated
-  to class \isa{idem}.%
-\end{isamarkuptext}%
-\isamarkuptrue%
-%
 \isamarkupsubsection{Abstract reasoning%
 }
 \isamarkuptrue%
@@ -700,48 +724,48 @@
   states that the function \isa{{\isacharparenleft}x\ {\isasymotimes}{\isacharparenright}} is injective:%
 \end{isamarkuptext}%
 \isamarkuptrue%
-\ \ \ \ \isacommand{lemma}\isamarkupfalse%
-\ {\isacharparenleft}\isakeyword{in}\ group{\isacharparenright}\ left{\isacharunderscore}cancel{\isacharcolon}\ {\isachardoublequoteopen}x\ {\isasymotimes}\ y\ {\isacharequal}\ x\ {\isasymotimes}\ z\ {\isasymlongleftrightarrow}\ y\ {\isacharequal}\ z{\isachardoublequoteclose}\isanewline
+%
+\isadelimquote
 %
-\isadelimproof
-\ \ \ \ %
-\endisadelimproof
+\endisadelimquote
 %
-\isatagproof
+\isatagquote
+\isacommand{lemma}\isamarkupfalse%
+\ {\isacharparenleft}\isakeyword{in}\ group{\isacharparenright}\ left{\isacharunderscore}cancel{\isacharcolon}\ {\isachardoublequoteopen}x\ {\isasymotimes}\ y\ {\isacharequal}\ x\ {\isasymotimes}\ z\ {\isasymlongleftrightarrow}\ y\ {\isacharequal}\ z{\isachardoublequoteclose}\isanewline
 \isacommand{proof}\isamarkupfalse%
 \isanewline
-\ \ \ \ \ \ \isacommand{assume}\isamarkupfalse%
+\ \ \isacommand{assume}\isamarkupfalse%
 \ {\isachardoublequoteopen}x\ {\isasymotimes}\ y\ {\isacharequal}\ x\ {\isasymotimes}\ z{\isachardoublequoteclose}\isanewline
-\ \ \ \ \ \ \isacommand{then}\isamarkupfalse%
+\ \ \isacommand{then}\isamarkupfalse%
 \ \isacommand{have}\isamarkupfalse%
 \ {\isachardoublequoteopen}x{\isasymdiv}\ {\isasymotimes}\ {\isacharparenleft}x\ {\isasymotimes}\ y{\isacharparenright}\ {\isacharequal}\ x{\isasymdiv}\ {\isasymotimes}\ {\isacharparenleft}x\ {\isasymotimes}\ z{\isacharparenright}{\isachardoublequoteclose}\ \isacommand{by}\isamarkupfalse%
 \ simp\isanewline
-\ \ \ \ \ \ \isacommand{then}\isamarkupfalse%
+\ \ \isacommand{then}\isamarkupfalse%
 \ \isacommand{have}\isamarkupfalse%
 \ {\isachardoublequoteopen}{\isacharparenleft}x{\isasymdiv}\ {\isasymotimes}\ x{\isacharparenright}\ {\isasymotimes}\ y\ {\isacharequal}\ {\isacharparenleft}x{\isasymdiv}\ {\isasymotimes}\ x{\isacharparenright}\ {\isasymotimes}\ z{\isachardoublequoteclose}\ \isacommand{using}\isamarkupfalse%
 \ assoc\ \isacommand{by}\isamarkupfalse%
 \ simp\isanewline
-\ \ \ \ \ \ \isacommand{then}\isamarkupfalse%
+\ \ \isacommand{then}\isamarkupfalse%
 \ \isacommand{show}\isamarkupfalse%
 \ {\isachardoublequoteopen}y\ {\isacharequal}\ z{\isachardoublequoteclose}\ \isacommand{using}\isamarkupfalse%
 \ neutl\ \isakeyword{and}\ invl\ \isacommand{by}\isamarkupfalse%
 \ simp\isanewline
-\ \ \ \ \isacommand{next}\isamarkupfalse%
+\isacommand{next}\isamarkupfalse%
 \isanewline
-\ \ \ \ \ \ \isacommand{assume}\isamarkupfalse%
+\ \ \isacommand{assume}\isamarkupfalse%
 \ {\isachardoublequoteopen}y\ {\isacharequal}\ z{\isachardoublequoteclose}\isanewline
-\ \ \ \ \ \ \isacommand{then}\isamarkupfalse%
+\ \ \isacommand{then}\isamarkupfalse%
 \ \isacommand{show}\isamarkupfalse%
 \ {\isachardoublequoteopen}x\ {\isasymotimes}\ y\ {\isacharequal}\ x\ {\isasymotimes}\ z{\isachardoublequoteclose}\ \isacommand{by}\isamarkupfalse%
 \ simp\isanewline
-\ \ \ \ \isacommand{qed}\isamarkupfalse%
+\isacommand{qed}\isamarkupfalse%
 %
-\endisatagproof
-{\isafoldproof}%
+\endisatagquote
+{\isafoldquote}%
 %
-\isadelimproof
+\isadelimquote
 %
-\endisadelimproof
+\endisadelimquote
 %
 \begin{isamarkuptext}%
 \noindent Here the \qt{\hyperlink{keyword.in}{\mbox{\isa{\isakeyword{in}}}} \isa{group}} target specification
@@ -760,10 +784,23 @@
   in locales:%
 \end{isamarkuptext}%
 \isamarkuptrue%
-\ \ \ \ \isacommand{primrec}\isamarkupfalse%
+%
+\isadelimquote
+%
+\endisadelimquote
+%
+\isatagquote
+\isacommand{primrec}\isamarkupfalse%
 \ {\isacharparenleft}\isakeyword{in}\ monoid{\isacharparenright}\ pow{\isacharunderscore}nat\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequoteopen}nat\ {\isasymRightarrow}\ {\isasymalpha}\ {\isasymRightarrow}\ {\isasymalpha}{\isachardoublequoteclose}\ \isakeyword{where}\isanewline
-\ \ \ \ \ \ {\isachardoublequoteopen}pow{\isacharunderscore}nat\ {\isadigit{0}}\ x\ {\isacharequal}\ {\isasymone}{\isachardoublequoteclose}\isanewline
-\ \ \ \ \ \ {\isacharbar}\ {\isachardoublequoteopen}pow{\isacharunderscore}nat\ {\isacharparenleft}Suc\ n{\isacharparenright}\ x\ {\isacharequal}\ x\ {\isasymotimes}\ pow{\isacharunderscore}nat\ n\ x{\isachardoublequoteclose}%
+\ \ {\isachardoublequoteopen}pow{\isacharunderscore}nat\ {\isadigit{0}}\ x\ {\isacharequal}\ {\isasymone}{\isachardoublequoteclose}\isanewline
+\ \ {\isacharbar}\ {\isachardoublequoteopen}pow{\isacharunderscore}nat\ {\isacharparenleft}Suc\ n{\isacharparenright}\ x\ {\isacharequal}\ x\ {\isasymotimes}\ pow{\isacharunderscore}nat\ n\ x{\isachardoublequoteclose}%
+\endisatagquote
+{\isafoldquote}%
+%
+\isadelimquote
+%
+\endisadelimquote
+%
 \begin{isamarkuptext}%
 \noindent If the locale \isa{group} is also a class, this local
   definition is propagated onto a global definition of
@@ -799,22 +836,22 @@
   of monoids for lists:%
 \end{isamarkuptext}%
 \isamarkuptrue%
-\ \ \ \ \isacommand{interpretation}\isamarkupfalse%
-\ list{\isacharunderscore}monoid{\isacharcolon}\ monoid\ {\isacharbrackleft}append\ {\isachardoublequoteopen}{\isacharbrackleft}{\isacharbrackright}{\isachardoublequoteclose}{\isacharbrackright}\isanewline
 %
-\isadelimproof
-\ \ \ \ \ \ %
-\endisadelimproof
+\isadelimquote
+%
+\endisadelimquote
 %
-\isatagproof
-\isacommand{by}\isamarkupfalse%
+\isatagquote
+\isacommand{interpretation}\isamarkupfalse%
+\ list{\isacharunderscore}monoid{\isacharcolon}\ monoid\ {\isacharbrackleft}append\ {\isachardoublequoteopen}{\isacharbrackleft}{\isacharbrackright}{\isachardoublequoteclose}{\isacharbrackright}\isanewline
+\ \ \isacommand{by}\isamarkupfalse%
 \ unfold{\isacharunderscore}locales\ auto%
-\endisatagproof
-{\isafoldproof}%
+\endisatagquote
+{\isafoldquote}%
 %
-\isadelimproof
+\isadelimquote
 %
-\endisadelimproof
+\endisadelimquote
 %
 \begin{isamarkuptext}%
 \noindent This enables us to apply facts on monoids
@@ -824,45 +861,45 @@
   be appropriate to map derived definitions accordingly:%
 \end{isamarkuptext}%
 \isamarkuptrue%
-\ \ \ \ \isacommand{fun}\isamarkupfalse%
+%
+\isadelimquote
+%
+\endisadelimquote
+%
+\isatagquote
+\isacommand{primrec}\isamarkupfalse%
 \ replicate\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequoteopen}nat\ {\isasymRightarrow}\ {\isasymalpha}\ list\ {\isasymRightarrow}\ {\isasymalpha}\ list{\isachardoublequoteclose}\ \isakeyword{where}\isanewline
-\ \ \ \ \ \ {\isachardoublequoteopen}replicate\ {\isadigit{0}}\ {\isacharunderscore}\ {\isacharequal}\ {\isacharbrackleft}{\isacharbrackright}{\isachardoublequoteclose}\isanewline
-\ \ \ \ \ \ {\isacharbar}\ {\isachardoublequoteopen}replicate\ {\isacharparenleft}Suc\ n{\isacharparenright}\ xs\ {\isacharequal}\ xs\ {\isacharat}\ replicate\ n\ xs{\isachardoublequoteclose}\isanewline
+\ \ {\isachardoublequoteopen}replicate\ {\isadigit{0}}\ {\isacharunderscore}\ {\isacharequal}\ {\isacharbrackleft}{\isacharbrackright}{\isachardoublequoteclose}\isanewline
+\ \ {\isacharbar}\ {\isachardoublequoteopen}replicate\ {\isacharparenleft}Suc\ n{\isacharparenright}\ xs\ {\isacharequal}\ xs\ {\isacharat}\ replicate\ n\ xs{\isachardoublequoteclose}\isanewline
 \isanewline
-\ \ \ \ \isacommand{interpretation}\isamarkupfalse%
+\isacommand{interpretation}\isamarkupfalse%
 \ 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
-\ \ \ \ %
-\endisadelimproof
-%
-\isatagproof
+\ \ {\isachardoublequoteopen}monoid{\isachardot}pow{\isacharunderscore}nat\ append\ {\isacharbrackleft}{\isacharbrackright}\ {\isacharequal}\ replicate{\isachardoublequoteclose}\isanewline
 \isacommand{proof}\isamarkupfalse%
 \ {\isacharminus}\isanewline
-\ \ \ \ \ \ \isacommand{interpret}\isamarkupfalse%
+\ \ \isacommand{interpret}\isamarkupfalse%
 \ monoid\ {\isacharbrackleft}append\ {\isachardoublequoteopen}{\isacharbrackleft}{\isacharbrackright}{\isachardoublequoteclose}{\isacharbrackright}\ \isacommand{{\isachardot}{\isachardot}}\isamarkupfalse%
 \isanewline
-\ \ \ \ \ \ \isacommand{show}\isamarkupfalse%
+\ \ \isacommand{show}\isamarkupfalse%
 \ {\isachardoublequoteopen}monoid{\isachardot}pow{\isacharunderscore}nat\ append\ {\isacharbrackleft}{\isacharbrackright}\ {\isacharequal}\ replicate{\isachardoublequoteclose}\isanewline
-\ \ \ \ \ \ \isacommand{proof}\isamarkupfalse%
+\ \ \isacommand{proof}\isamarkupfalse%
 \isanewline
-\ \ \ \ \ \ \ \ \isacommand{fix}\isamarkupfalse%
+\ \ \ \ \isacommand{fix}\isamarkupfalse%
 \ n\isanewline
-\ \ \ \ \ \ \ \ \isacommand{show}\isamarkupfalse%
+\ \ \ \ \isacommand{show}\isamarkupfalse%
 \ {\isachardoublequoteopen}monoid{\isachardot}pow{\isacharunderscore}nat\ append\ {\isacharbrackleft}{\isacharbrackright}\ n\ {\isacharequal}\ replicate\ n{\isachardoublequoteclose}\isanewline
-\ \ \ \ \ \ \ \ \ \ \isacommand{by}\isamarkupfalse%
+\ \ \ \ \ \ \isacommand{by}\isamarkupfalse%
 \ {\isacharparenleft}induct\ n{\isacharparenright}\ auto\isanewline
-\ \ \ \ \ \ \isacommand{qed}\isamarkupfalse%
+\ \ \isacommand{qed}\isamarkupfalse%
 \isanewline
-\ \ \ \ \isacommand{qed}\isamarkupfalse%
+\isacommand{qed}\isamarkupfalse%
 \ intro{\isacharunderscore}locales%
-\endisatagproof
-{\isafoldproof}%
+\endisatagquote
+{\isafoldquote}%
 %
-\isadelimproof
+\isadelimquote
 %
-\endisadelimproof
+\endisadelimquote
 %
 \isamarkupsubsection{Additional subclass relations%
 }
@@ -875,38 +912,38 @@
   together with a proof of the logical difference:%
 \end{isamarkuptext}%
 \isamarkuptrue%
-\ \ \ \ \isacommand{subclass}\isamarkupfalse%
-\ {\isacharparenleft}\isakeyword{in}\ group{\isacharparenright}\ monoid\isanewline
+%
+\isadelimquote
 %
-\isadelimproof
-\ \ \ \ %
-\endisadelimproof
+\endisadelimquote
 %
-\isatagproof
+\isatagquote
+\isacommand{subclass}\isamarkupfalse%
+\ {\isacharparenleft}\isakeyword{in}\ group{\isacharparenright}\ monoid\isanewline
 \isacommand{proof}\isamarkupfalse%
 \ unfold{\isacharunderscore}locales\isanewline
-\ \ \ \ \ \ \isacommand{fix}\isamarkupfalse%
+\ \ \isacommand{fix}\isamarkupfalse%
 \ x\isanewline
-\ \ \ \ \ \ \isacommand{from}\isamarkupfalse%
+\ \ \isacommand{from}\isamarkupfalse%
 \ invl\ \isacommand{have}\isamarkupfalse%
 \ {\isachardoublequoteopen}x{\isasymdiv}\ {\isasymotimes}\ x\ {\isacharequal}\ {\isasymone}{\isachardoublequoteclose}\ \isacommand{by}\isamarkupfalse%
 \ simp\isanewline
-\ \ \ \ \ \ \isacommand{with}\isamarkupfalse%
+\ \ \isacommand{with}\isamarkupfalse%
 \ assoc\ {\isacharbrackleft}symmetric{\isacharbrackright}\ neutl\ invl\ \isacommand{have}\isamarkupfalse%
 \ {\isachardoublequoteopen}x{\isasymdiv}\ {\isasymotimes}\ {\isacharparenleft}x\ {\isasymotimes}\ {\isasymone}{\isacharparenright}\ {\isacharequal}\ x{\isasymdiv}\ {\isasymotimes}\ x{\isachardoublequoteclose}\ \isacommand{by}\isamarkupfalse%
 \ simp\isanewline
-\ \ \ \ \ \ \isacommand{with}\isamarkupfalse%
+\ \ \isacommand{with}\isamarkupfalse%
 \ left{\isacharunderscore}cancel\ \isacommand{show}\isamarkupfalse%
 \ {\isachardoublequoteopen}x\ {\isasymotimes}\ {\isasymone}\ {\isacharequal}\ x{\isachardoublequoteclose}\ \isacommand{by}\isamarkupfalse%
 \ simp\isanewline
-\ \ \ \ \isacommand{qed}\isamarkupfalse%
+\isacommand{qed}\isamarkupfalse%
 %
-\endisatagproof
-{\isafoldproof}%
+\endisatagquote
+{\isafoldquote}%
 %
-\isadelimproof
+\isadelimquote
 %
-\endisadelimproof
+\endisadelimquote
 %
 \begin{isamarkuptext}%
 \noindent The logical proof is carried out on the locale level
@@ -1006,24 +1043,11 @@
 \ {\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%