# HG changeset patch
# User haftmann
# Date 1193406143 -7200
# Node ID f1d2e106f2fe01a13aa7bb9bc488d53f9548e92c
# Parent  e83c6c43f1e6745f25425ee17db9996ce2e120d4
adjusted

diff -r e83c6c43f1e6 -r f1d2e106f2fe doc-src/IsarAdvanced/Classes/Thy/Classes.thy
--- a/doc-src/IsarAdvanced/Classes/Thy/Classes.thy	Fri Oct 26 15:37:02 2007 +0200
+++ b/doc-src/IsarAdvanced/Classes/Thy/Classes.thy	Fri Oct 26 15:42:23 2007 +0200
@@ -12,16 +12,6 @@
 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)
-  "_gamma" :: "type"  ("\<gamma>")
-  "_gamma_ofsort" :: "sort \<Rightarrow> type"  ("\<gamma>()\<Colon>_" [0] 1000)
-  "_alpha_f" :: "type"  ("\<alpha>\<^sub>f")
-  "_alpha_f_ofsort" :: "sort \<Rightarrow> type"  ("\<alpha>\<^sub>f()\<Colon>_" [0] 1000)
-  "_beta_f" :: "type"  ("\<beta>\<^sub>f")
-  "_beta_f_ofsort" :: "sort \<Rightarrow> type"  ("\<beta>\<^sub>f()\<Colon>_" [0] 1000)
-  "_gamma_f" :: "type"  ("\<gamma>\<^sub>f")
-  "_gamma_ofsort_f" :: "sort \<Rightarrow> type"  ("\<gamma>\<^sub>f()\<Colon>_" [0] 1000)
 
 parse_ast_translation {*
   let
@@ -30,38 +20,8 @@
     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);
-    fun gamma_ast_tr [] = Syntax.Variable "'c"
-      | gamma_ast_tr asts = raise Syntax.AST ("gamma_ast_tr", asts);
-    fun gamma_ofsort_ast_tr [ast] =
-      Syntax.Appl [Syntax.Constant "_ofsort", Syntax.Variable "'c", ast]
-      | gamma_ofsort_ast_tr asts = raise Syntax.AST ("gamma_ast_tr", asts);
-    fun alpha_f_ast_tr [] = Syntax.Variable "'a_f"
-      | alpha_f_ast_tr asts = raise Syntax.AST ("alpha_f_ast_tr", asts);
-    fun alpha_f_ofsort_ast_tr [ast] =
-      Syntax.Appl [Syntax.Constant "_ofsort", Syntax.Variable "'a_f", ast]
-      | alpha_f_ofsort_ast_tr asts = raise Syntax.AST ("alpha_f_ast_tr", asts);
-    fun beta_f_ast_tr [] = Syntax.Variable "'b_f"
-      | beta_f_ast_tr asts = raise Syntax.AST ("beta_f_ast_tr", asts);
-    fun beta_f_ofsort_ast_tr [ast] =
-      Syntax.Appl [Syntax.Constant "_ofsort", Syntax.Variable "'b_f", ast]
-      | beta_f_ofsort_ast_tr asts = raise Syntax.AST ("beta_f_ast_tr", asts);
-    fun gamma_f_ast_tr [] = Syntax.Variable "'c_f"
-      | gamma_f_ast_tr asts = raise Syntax.AST ("gamma_f_ast_tr", asts);
-    fun gamma_f_ofsort_ast_tr [ast] =
-      Syntax.Appl [Syntax.Constant "_ofsort", Syntax.Variable "'c_f", ast]
-      | gamma_f_ofsort_ast_tr asts = raise Syntax.AST ("gamma_f_ast_tr", asts);
   in [
-    ("_alpha", alpha_ast_tr), ("_alpha_ofsort", alpha_ofsort_ast_tr),
-    ("_beta", beta_ast_tr), ("_beta_ofsort", beta_ofsort_ast_tr),
-    ("_gamma", gamma_ast_tr), ("_gamma_ofsort", gamma_ofsort_ast_tr),
-    ("_alpha_f", alpha_f_ast_tr), ("_alpha_f_ofsort", alpha_f_ofsort_ast_tr),
-    ("_beta_f", beta_f_ast_tr), ("_beta_f_ofsort", beta_f_ofsort_ast_tr),
-    ("_gamma_f", gamma_f_ast_tr), ("_gamma_f_ofsort", gamma_f_ofsort_ast_tr)
+    ("_alpha", alpha_ast_tr), ("_alpha_ofsort", alpha_ofsort_ast_tr)
   ] end
 *}
 (*>*)
@@ -164,8 +124,8 @@
 *}
 
     class semigroup = type +
-      fixes mult :: "\<alpha> \<Rightarrow> \<alpha> \<Rightarrow> \<alpha>"    (infixl "\<^loc>\<otimes>" 70)
-      assumes assoc: "(x \<^loc>\<otimes> y) \<^loc>\<otimes> z = x \<^loc>\<otimes> (y \<^loc>\<otimes> z)"
+      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
@@ -242,8 +202,8 @@
 *}
 
     class monoidl = semigroup +
-      fixes neutral :: "\<alpha>" ("\<^loc>\<one>")
-      assumes neutl: "\<^loc>\<one> \<^loc>\<otimes> x = x"
+      fixes neutral :: "\<alpha>" ("\<one>")
+      assumes neutl: "\<one> \<otimes> x = x"
 
 text {*
   \noindent Again, we make some instances, by
@@ -283,7 +243,7 @@
 *}
 
     class monoid = monoidl +
-      assumes neutr: "x \<^loc>\<otimes> \<^loc>\<one> = x"
+      assumes neutr: "x \<otimes> \<one> = x"
 
 text {*
   \noindent Instantiations may also be given simultaneously for different
@@ -313,8 +273,8 @@
 *}
 
     class group = monoidl +
-      fixes inverse :: "\<alpha> \<Rightarrow> \<alpha>"    ("(_\<^loc>\<div>)" [1000] 999)
-      assumes invl: "x\<^loc>\<div> \<^loc>\<otimes> x = \<^loc>\<one>"
+      fixes inverse :: "\<alpha> \<Rightarrow> \<alpha>"    ("(_\<div>)" [1000] 999)
+      assumes invl: "x\<div> \<otimes> x = \<one>"
 
     instance int :: group
       inverse_int_def: "i\<div> \<equiv> - i"
@@ -381,15 +341,15 @@
   states that the function @{text "(x \<circ>)"} is injective:
 *}
 
-    lemma (in group) left_cancel: "x \<^loc>\<otimes> y = x \<^loc>\<otimes> z \<longleftrightarrow> y = z"
+    lemma (in group) left_cancel: "x \<otimes> y = x \<otimes> z \<longleftrightarrow> y = z"
     proof
-    assume "x \<^loc>\<otimes> y = x \<^loc>\<otimes> z"
-      then have "x\<^loc>\<div> \<^loc>\<otimes> (x \<^loc>\<otimes> y) = x\<^loc>\<div> \<^loc>\<otimes> (x \<^loc>\<otimes> z)" by simp
-      then have "(x\<^loc>\<div> \<^loc>\<otimes> x) \<^loc>\<otimes> y = (x\<^loc>\<div> \<^loc>\<otimes> x) \<^loc>\<otimes> z" using assoc by simp
+    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 \<^loc>\<otimes> y = x \<^loc>\<otimes> z" by simp
+      then show "x \<otimes> y = x \<otimes> z" by simp
     qed
 
 text {*
@@ -412,8 +372,8 @@
 
     fun (in monoid)
       pow_nat :: "nat \<Rightarrow> \<alpha> \<Rightarrow> \<alpha>" where
-      "pow_nat 0 x = \<^loc>\<one>"
-      | "pow_nat (Suc n) x = x \<^loc>\<otimes> pow_nat n x"
+      "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
@@ -440,16 +400,16 @@
     subclass (in group) monoid
     proof unfold_locales
       fix x
-      from invl have "x\<^loc>\<div> \<^loc>\<otimes> x = \<^loc>\<one>" by simp
-      with assoc [symmetric] neutl invl have "x\<^loc>\<div> \<^loc>\<otimes> (x \<^loc>\<otimes> \<^loc>\<one>) = x\<^loc>\<div> \<^loc>\<otimes> x" by simp
-      with left_cancel show "x \<^loc>\<otimes> \<^loc>\<one> = x" by simp
+      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 {*
-  The logical proof is carried out on the locale level
+  \noindent The logical proof is carried out on the locale level
   and thus conveniently is opened using the @{text unfold_locales}
   method which only leaves the logical differences still
-  open to proof to the user.  After the proof it is propagated
+  open to proof to the user.  Afterwards it is propagated
   to the type system, making @{text group} an instance of
   @{text monoid}.  For illustration, a derived definition
   in @{text group} which uses @{text pow_nat}:
@@ -459,10 +419,10 @@
       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)\<^loc>\<div>)"
+        else (pow_nat (nat (- k)) x)\<div>)"
 
 text {*
-  yields the global definition of
+  \noindent   yields the global definition of
   @{term [source] "pow_int \<Colon> int \<Rightarrow> \<alpha>\<Colon>group \<Rightarrow> \<alpha>\<Colon>group"}
   with the corresponding theorem @{thm pow_int_def [no_vars]}.
 *}
diff -r e83c6c43f1e6 -r f1d2e106f2fe doc-src/IsarAdvanced/Classes/Thy/code_examples/Classes.hs
--- a/doc-src/IsarAdvanced/Classes/Thy/code_examples/Classes.hs	Fri Oct 26 15:37:02 2007 +0200
+++ b/doc-src/IsarAdvanced/Classes/Thy/code_examples/Classes.hs	Fri Oct 26 15:42:23 2007 +0200
@@ -1,29 +1,28 @@
 module Classes where {
 
 
-data Nat = Suc Classes.Nat | Zero_nat;
+data Nat = Suc Nat | Zero_nat;
 
 data Bit = B1 | B0;
 
-nat_aux :: Integer -> Classes.Nat -> Classes.Nat;
-nat_aux i n =
-  (if i <= 0 then n else Classes.nat_aux (i - 1) (Classes.Suc n));
+nat_aux :: Integer -> Nat -> Nat;
+nat_aux i n = (if i <= 0 then n else nat_aux (i - 1) (Suc n));
 
-nat :: Integer -> Classes.Nat;
-nat i = Classes.nat_aux i Classes.Zero_nat;
+nat :: Integer -> Nat;
+nat i = nat_aux i Zero_nat;
 
 class Semigroup a where {
   mult :: a -> a -> a;
 };
 
-class (Classes.Semigroup a) => Monoidl a where {
+class (Semigroup a) => Monoidl a where {
   neutral :: a;
 };
 
-class (Classes.Monoidl a) => Monoid a where {
+class (Monoidl a) => Monoid a where {
 };
 
-class (Classes.Monoid a) => Group a where {
+class (Monoid a) => Group a where {
   inverse :: a -> a;
 };
 
@@ -36,31 +35,31 @@
 mult_int :: Integer -> Integer -> Integer;
 mult_int i j = i + j;
 
-instance Classes.Semigroup Integer where {
-  mult = Classes.mult_int;
+instance Semigroup Integer where {
+  mult = mult_int;
 };
 
-instance Classes.Monoidl Integer where {
-  neutral = Classes.neutral_int;
+instance Monoidl Integer where {
+  neutral = neutral_int;
 };
 
-instance Classes.Monoid Integer where {
+instance Monoid Integer where {
 };
 
-instance Classes.Group Integer where {
-  inverse = Classes.inverse_int;
+instance Group Integer where {
+  inverse = inverse_int;
 };
 
-pow_nat :: (Classes.Monoid a) => Classes.Nat -> a -> a;
-pow_nat (Classes.Suc n) x = Classes.mult x (Classes.pow_nat n x);
-pow_nat Classes.Zero_nat x = Classes.neutral;
+pow_nat :: (Monoid a) => Nat -> a -> a;
+pow_nat (Suc n) x = mult x (pow_nat n x);
+pow_nat Zero_nat x = neutral;
 
-pow_int :: (Classes.Group a) => Integer -> a -> a;
+pow_int :: (Group a) => Integer -> a -> a;
 pow_int k x =
-  (if 0 <= k then Classes.pow_nat (Classes.nat k) x
-    else Classes.inverse (Classes.pow_nat (Classes.nat (negate k)) x));
+  (if 0 <= k then pow_nat (nat k) x
+    else inverse (pow_nat (nat (negate k)) x));
 
 example :: Integer;
-example = Classes.pow_int 10 (-2);
+example = pow_int 10 (-2);
 
 }
diff -r e83c6c43f1e6 -r f1d2e106f2fe doc-src/IsarAdvanced/Classes/Thy/document/Classes.tex
--- a/doc-src/IsarAdvanced/Classes/Thy/document/Classes.tex	Fri Oct 26 15:37:02 2007 +0200
+++ b/doc-src/IsarAdvanced/Classes/Thy/document/Classes.tex	Fri Oct 26 15:42:23 2007 +0200
@@ -148,8 +148,8 @@
 \isamarkuptrue%
 \ \ \ \ \isacommand{class}\isamarkupfalse%
 \ semigroup\ {\isacharequal}\ type\ {\isacharplus}\isanewline
-\ \ \ \ \ \ \isakeyword{fixes}\ mult\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequoteopen}{\isasymalpha}\ {\isasymRightarrow}\ {\isasymalpha}\ {\isasymRightarrow}\ {\isasymalpha}{\isachardoublequoteclose}\ \ \ \ {\isacharparenleft}\isakeyword{infixl}\ {\isachardoublequoteopen}\isactrlloc {\isasymotimes}{\isachardoublequoteclose}\ {\isadigit{7}}{\isadigit{0}}{\isacharparenright}\isanewline
-\ \ \ \ \ \ \isakeyword{assumes}\ assoc{\isacharcolon}\ {\isachardoublequoteopen}{\isacharparenleft}x\ \isactrlloc {\isasymotimes}\ y{\isacharparenright}\ \isactrlloc {\isasymotimes}\ z\ {\isacharequal}\ x\ \isactrlloc {\isasymotimes}\ {\isacharparenleft}y\ \isactrlloc {\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}%
 \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
@@ -291,8 +291,8 @@
 \isamarkuptrue%
 \ \ \ \ \isacommand{class}\isamarkupfalse%
 \ monoidl\ {\isacharequal}\ semigroup\ {\isacharplus}\isanewline
-\ \ \ \ \ \ \isakeyword{fixes}\ neutral\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequoteopen}{\isasymalpha}{\isachardoublequoteclose}\ {\isacharparenleft}{\isachardoublequoteopen}\isactrlloc {\isasymone}{\isachardoublequoteclose}{\isacharparenright}\isanewline
-\ \ \ \ \ \ \isakeyword{assumes}\ neutl{\isacharcolon}\ {\isachardoublequoteopen}\isactrlloc {\isasymone}\ \isactrlloc {\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}%
 \begin{isamarkuptext}%
 \noindent Again, we make some instances, by
   providing suitable parameter definitions and proofs for the
@@ -401,7 +401,7 @@
 \isamarkuptrue%
 \ \ \ \ \isacommand{class}\isamarkupfalse%
 \ monoid\ {\isacharequal}\ monoidl\ {\isacharplus}\isanewline
-\ \ \ \ \ \ \isakeyword{assumes}\ neutr{\isacharcolon}\ {\isachardoublequoteopen}x\ \isactrlloc {\isasymotimes}\ \isactrlloc {\isasymone}\ {\isacharequal}\ x{\isachardoublequoteclose}%
+\ \ \ \ \ \ \isakeyword{assumes}\ neutr{\isacharcolon}\ {\isachardoublequoteopen}x\ {\isasymotimes}\ {\isasymone}\ {\isacharequal}\ x{\isachardoublequoteclose}%
 \begin{isamarkuptext}%
 \noindent Instantiations may also be given simultaneously for different
   type constructors:%
@@ -470,8 +470,8 @@
 \isamarkuptrue%
 \ \ \ \ \isacommand{class}\isamarkupfalse%
 \ group\ {\isacharequal}\ monoidl\ {\isacharplus}\isanewline
-\ \ \ \ \ \ \isakeyword{fixes}\ inverse\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequoteopen}{\isasymalpha}\ {\isasymRightarrow}\ {\isasymalpha}{\isachardoublequoteclose}\ \ \ \ {\isacharparenleft}{\isachardoublequoteopen}{\isacharparenleft}{\isacharunderscore}\isactrlloc {\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\isactrlloc {\isasymdiv}\ \isactrlloc {\isasymotimes}\ x\ {\isacharequal}\ \isactrlloc {\isasymone}{\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%
 \ int\ {\isacharcolon}{\isacharcolon}\ group\isanewline
@@ -612,7 +612,7 @@
 \end{isamarkuptext}%
 \isamarkuptrue%
 \ \ \ \ \isacommand{lemma}\isamarkupfalse%
-\ {\isacharparenleft}\isakeyword{in}\ group{\isacharparenright}\ left{\isacharunderscore}cancel{\isacharcolon}\ {\isachardoublequoteopen}x\ \isactrlloc {\isasymotimes}\ y\ {\isacharequal}\ x\ \isactrlloc {\isasymotimes}\ z\ {\isasymlongleftrightarrow}\ y\ {\isacharequal}\ z{\isachardoublequoteclose}\isanewline
+\ {\isacharparenleft}\isakeyword{in}\ group{\isacharparenright}\ left{\isacharunderscore}cancel{\isacharcolon}\ {\isachardoublequoteopen}x\ {\isasymotimes}\ y\ {\isacharequal}\ x\ {\isasymotimes}\ z\ {\isasymlongleftrightarrow}\ y\ {\isacharequal}\ z{\isachardoublequoteclose}\isanewline
 %
 \isadelimproof
 \ \ \ \ %
@@ -622,14 +622,14 @@
 \isacommand{proof}\isamarkupfalse%
 \isanewline
 \ \ \ \ \isacommand{assume}\isamarkupfalse%
-\ {\isachardoublequoteopen}x\ \isactrlloc {\isasymotimes}\ y\ {\isacharequal}\ x\ \isactrlloc {\isasymotimes}\ z{\isachardoublequoteclose}\isanewline
+\ {\isachardoublequoteopen}x\ {\isasymotimes}\ y\ {\isacharequal}\ x\ {\isasymotimes}\ z{\isachardoublequoteclose}\isanewline
 \ \ \ \ \ \ \isacommand{then}\isamarkupfalse%
 \ \isacommand{have}\isamarkupfalse%
-\ {\isachardoublequoteopen}x\isactrlloc {\isasymdiv}\ \isactrlloc {\isasymotimes}\ {\isacharparenleft}x\ \isactrlloc {\isasymotimes}\ y{\isacharparenright}\ {\isacharequal}\ x\isactrlloc {\isasymdiv}\ \isactrlloc {\isasymotimes}\ {\isacharparenleft}x\ \isactrlloc {\isasymotimes}\ z{\isacharparenright}{\isachardoublequoteclose}\ \isacommand{by}\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{have}\isamarkupfalse%
-\ {\isachardoublequoteopen}{\isacharparenleft}x\isactrlloc {\isasymdiv}\ \isactrlloc {\isasymotimes}\ x{\isacharparenright}\ \isactrlloc {\isasymotimes}\ y\ {\isacharequal}\ {\isacharparenleft}x\isactrlloc {\isasymdiv}\ \isactrlloc {\isasymotimes}\ x{\isacharparenright}\ \isactrlloc {\isasymotimes}\ z{\isachardoublequoteclose}\ \isacommand{using}\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%
@@ -643,7 +643,7 @@
 \ {\isachardoublequoteopen}y\ {\isacharequal}\ z{\isachardoublequoteclose}\isanewline
 \ \ \ \ \ \ \isacommand{then}\isamarkupfalse%
 \ \isacommand{show}\isamarkupfalse%
-\ {\isachardoublequoteopen}x\ \isactrlloc {\isasymotimes}\ y\ {\isacharequal}\ x\ \isactrlloc {\isasymotimes}\ z{\isachardoublequoteclose}\ \isacommand{by}\isamarkupfalse%
+\ {\isachardoublequoteopen}x\ {\isasymotimes}\ y\ {\isacharequal}\ x\ {\isasymotimes}\ z{\isachardoublequoteclose}\ \isacommand{by}\isamarkupfalse%
 \ simp\isanewline
 \ \ \ \ \isacommand{qed}\isamarkupfalse%
 %
@@ -674,8 +674,8 @@
 \ \ \ \ \isacommand{fun}\isamarkupfalse%
 \ {\isacharparenleft}\isakeyword{in}\ monoid{\isacharparenright}\isanewline
 \ \ \ \ \ \ pow{\isacharunderscore}nat\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequoteopen}nat\ {\isasymRightarrow}\ {\isasymalpha}\ {\isasymRightarrow}\ {\isasymalpha}{\isachardoublequoteclose}\ \isakeyword{where}\isanewline
-\ \ \ \ \ \ {\isachardoublequoteopen}pow{\isacharunderscore}nat\ {\isadigit{0}}\ x\ {\isacharequal}\ \isactrlloc {\isasymone}{\isachardoublequoteclose}\isanewline
-\ \ \ \ \ \ {\isacharbar}\ {\isachardoublequoteopen}pow{\isacharunderscore}nat\ {\isacharparenleft}Suc\ n{\isacharparenright}\ x\ {\isacharequal}\ x\ \isactrlloc {\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}%
 \begin{isamarkuptext}%
 \noindent If the locale \isa{group} is also a class, this local
   definition is propagated onto a global definition of
@@ -715,15 +715,15 @@
 \ x\isanewline
 \ \ \ \ \ \ \isacommand{from}\isamarkupfalse%
 \ invl\ \isacommand{have}\isamarkupfalse%
-\ {\isachardoublequoteopen}x\isactrlloc {\isasymdiv}\ \isactrlloc {\isasymotimes}\ x\ {\isacharequal}\ \isactrlloc {\isasymone}{\isachardoublequoteclose}\ \isacommand{by}\isamarkupfalse%
+\ {\isachardoublequoteopen}x{\isasymdiv}\ {\isasymotimes}\ x\ {\isacharequal}\ {\isasymone}{\isachardoublequoteclose}\ \isacommand{by}\isamarkupfalse%
 \ simp\isanewline
 \ \ \ \ \ \ \isacommand{with}\isamarkupfalse%
 \ assoc\ {\isacharbrackleft}symmetric{\isacharbrackright}\ neutl\ invl\ \isacommand{have}\isamarkupfalse%
-\ {\isachardoublequoteopen}x\isactrlloc {\isasymdiv}\ \isactrlloc {\isasymotimes}\ {\isacharparenleft}x\ \isactrlloc {\isasymotimes}\ \isactrlloc {\isasymone}{\isacharparenright}\ {\isacharequal}\ x\isactrlloc {\isasymdiv}\ \isactrlloc {\isasymotimes}\ x{\isachardoublequoteclose}\ \isacommand{by}\isamarkupfalse%
+\ {\isachardoublequoteopen}x{\isasymdiv}\ {\isasymotimes}\ {\isacharparenleft}x\ {\isasymotimes}\ {\isasymone}{\isacharparenright}\ {\isacharequal}\ x{\isasymdiv}\ {\isasymotimes}\ x{\isachardoublequoteclose}\ \isacommand{by}\isamarkupfalse%
 \ simp\isanewline
 \ \ \ \ \ \ \isacommand{with}\isamarkupfalse%
 \ left{\isacharunderscore}cancel\ \isacommand{show}\isamarkupfalse%
-\ {\isachardoublequoteopen}x\ \isactrlloc {\isasymotimes}\ \isactrlloc {\isasymone}\ {\isacharequal}\ x{\isachardoublequoteclose}\ \isacommand{by}\isamarkupfalse%
+\ {\isachardoublequoteopen}x\ {\isasymotimes}\ {\isasymone}\ {\isacharequal}\ x{\isachardoublequoteclose}\ \isacommand{by}\isamarkupfalse%
 \ simp\isanewline
 \ \ \ \ \isacommand{qed}\isamarkupfalse%
 %
@@ -735,10 +735,10 @@
 \endisadelimproof
 %
 \begin{isamarkuptext}%
-The logical proof is carried out on the locale level
+\noindent The logical proof is carried out on the locale level
   and thus conveniently is opened using the \isa{unfold{\isacharunderscore}locales}
   method which only leaves the logical differences still
-  open to proof to the user.  After the proof it is propagated
+  open to proof to the user.  Afterwards it is propagated
   to the type system, making \isa{group} an instance of
   \isa{monoid}.  For illustration, a derived definition
   in \isa{group} which uses \isa{pow{\isacharunderscore}nat}:%
@@ -749,9 +749,9 @@
 \ \ \ \ \ \ 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}\isactrlloc {\isasymdiv}{\isacharparenright}{\isachardoublequoteclose}%
+\ \ \ \ \ \ \ \ else\ {\isacharparenleft}pow{\isacharunderscore}nat\ {\isacharparenleft}nat\ {\isacharparenleft}{\isacharminus}\ k{\isacharparenright}{\isacharparenright}\ x{\isacharparenright}{\isasymdiv}{\isacharparenright}{\isachardoublequoteclose}%
 \begin{isamarkuptext}%
-yields the global definition of
+\noindent   yields the global definition of
   \isa{{\isachardoublequote}pow{\isacharunderscore}int\ {\isasymColon}\ int\ {\isasymRightarrow}\ {\isasymalpha}{\isasymColon}group\ {\isasymRightarrow}\ {\isasymalpha}{\isasymColon}group{\isachardoublequote}}
   with the corresponding theorem \isa{pow{\isacharunderscore}int\ k\ x\ {\isacharequal}\ {\isacharparenleft}if\ {\isadigit{0}}\ {\isasymle}\ k\ then\ pow{\isacharunderscore}nat\ {\isacharparenleft}nat\ k{\isacharparenright}\ x\ else\ {\isacharparenleft}pow{\isacharunderscore}nat\ {\isacharparenleft}nat\ {\isacharparenleft}{\isacharminus}\ k{\isacharparenright}{\isacharparenright}\ x{\isacharparenright}{\isasymdiv}{\isacharparenright}}.%
 \end{isamarkuptext}%
diff -r e83c6c43f1e6 -r f1d2e106f2fe doc-src/IsarAdvanced/Classes/Thy/document/isabelle.sty
--- a/doc-src/IsarAdvanced/Classes/Thy/document/isabelle.sty	Fri Oct 26 15:37:02 2007 +0200
+++ b/doc-src/IsarAdvanced/Classes/Thy/document/isabelle.sty	Fri Oct 26 15:42:23 2007 +0200
@@ -25,10 +25,10 @@
 \newcommand{\isactrlsup}[1]{\emph{\isascriptstyle${}\sp{#1}$}}
 \newcommand{\isactrlisub}[1]{\emph{\isascriptstyle${}\sb{#1}$}}
 \newcommand{\isactrlisup}[1]{\emph{\isascriptstyle${}\sp{#1}$}}
-\newcommand{\isactrlbsub}{\emph\bgroup\begin{math}{}\sb\bgroup\mbox\bgroup\isastylescript}
-\newcommand{\isactrlesub}{\egroup\egroup\end{math}\egroup}
-\newcommand{\isactrlbsup}{\emph\bgroup\begin{math}{}\sp\bgroup\mbox\bgroup\isastylescript}
-\newcommand{\isactrlesup}{\egroup\egroup\end{math}\egroup}
+\DeclareRobustCommand{\isactrlbsub}{\emph\bgroup\math{}\sb\bgroup\mbox\bgroup\isastylescript}
+\DeclareRobustCommand{\isactrlesub}{\egroup\egroup\endmath\egroup}
+\DeclareRobustCommand{\isactrlbsup}{\emph\bgroup\math{}\sp\bgroup\mbox\bgroup\isastylescript}
+\DeclareRobustCommand{\isactrlesup}{\egroup\egroup\endmath\egroup}
 \newcommand{\isactrlbold}[1]{{\bfseries\upshape\boldmath#1}}
 \newcommand{\isactrlloc}[1]{{\bfseries\upshape\boldmath#1}}
 \newenvironment{isaantiq}{{\isacharat\isacharbraceleft}}{{\isacharbraceright}}