# HG changeset patch
# User haftmann
# Date 1276580497 -7200
# Node ID e732b4f8fddf1643c443f41c62d57570b375b3dd
# Parent  e9004a3e0d940cdd27146926df12d75d2f686f3c
tuned documents

diff -r e9004a3e0d94 -r e732b4f8fddf doc-src/Codegen/Thy/Further.thy
--- a/doc-src/Codegen/Thy/Further.thy	Mon Jun 14 16:00:47 2010 +0200
+++ b/doc-src/Codegen/Thy/Further.thy	Tue Jun 15 07:41:37 2010 +0200
@@ -81,7 +81,7 @@
 interpretation %quote fun_power: power "\<lambda>n (f :: 'a \<Rightarrow> 'a). f ^^ n" where
   "power.powers (\<lambda>n f. f ^^ n) = funpows"
   by unfold_locales
-    (simp_all add: expand_fun_eq funpow_mult [symmetric] mult_commute funpows_def)
+    (simp_all add: expand_fun_eq funpow_mult mult_commute funpows_def)
 
 text {*
   \noindent This additional equation is trivially proved by the definition
diff -r e9004a3e0d94 -r e732b4f8fddf doc-src/Codegen/Thy/document/Further.tex
--- a/doc-src/Codegen/Thy/document/Further.tex	Mon Jun 14 16:00:47 2010 +0200
+++ b/doc-src/Codegen/Thy/document/Further.tex	Tue Jun 15 07:41:37 2010 +0200
@@ -36,27 +36,6 @@
 \isamarkupsubsection{Locales and interpretation%
 }
 \isamarkuptrue%
-\isacommand{lemma}\isamarkupfalse%
-\ funpow{\isacharunderscore}mult{\isacharcolon}\ %
-\isamarkupcmt{FIXME%
-}
-\isanewline
-\ \ \isakeyword{fixes}\ f\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequoteopen}{\isacharprime}a\ {\isasymRightarrow}\ {\isacharprime}a{\isachardoublequoteclose}\isanewline
-\ \ \isakeyword{shows}\ {\isachardoublequoteopen}{\isacharparenleft}f\ {\isacharcircum}{\isacharcircum}\ m{\isacharparenright}\ {\isacharcircum}{\isacharcircum}\ n\ {\isacharequal}\ f\ {\isacharcircum}{\isacharcircum}\ {\isacharparenleft}m\ {\isacharasterisk}\ n{\isacharparenright}{\isachardoublequoteclose}\isanewline
-%
-\isadelimproof
-\ \ %
-\endisadelimproof
-%
-\isatagproof
-\isacommand{by}\isamarkupfalse%
-\ {\isacharparenleft}induct\ n{\isacharparenright}\ {\isacharparenleft}simp{\isacharunderscore}all\ add{\isacharcolon}\ funpow{\isacharunderscore}add{\isacharparenright}%
-\endisatagproof
-{\isafoldproof}%
-%
-\isadelimproof
-%
-\endisadelimproof
 %
 \begin{isamarkuptext}%
 A technical issue comes to surface when generating code from
@@ -202,8 +181,8 @@
 \isatypewriter%
 \noindent%
 \hspace*{0pt}funpow ::~forall a.~Nat -> (a -> a) -> a -> a;\\
+\hspace*{0pt}funpow Zero{\char95}nat f = id;\\
 \hspace*{0pt}funpow (Suc n) f = f .~funpow n f;\\
-\hspace*{0pt}funpow Zero{\char95}nat f = id;\\
 \hspace*{0pt}\\
 \hspace*{0pt}funpows ::~forall a.~[Nat] -> (a -> a) -> a -> a;\\
 \hspace*{0pt}funpows [] = id;\\
diff -r e9004a3e0d94 -r e732b4f8fddf doc-src/Codegen/Thy/document/Program.tex
--- a/doc-src/Codegen/Thy/document/Program.tex	Mon Jun 14 16:00:47 2010 +0200
+++ b/doc-src/Codegen/Thy/document/Program.tex	Tue Jun 15 07:41:37 2010 +0200
@@ -342,7 +342,7 @@
 \hspace*{0pt} ~type 'a semigroup\\
 \hspace*{0pt} ~val mult :~'a semigroup -> 'a -> 'a -> 'a\\
 \hspace*{0pt} ~type 'a monoid\\
-\hspace*{0pt} ~val monoid{\char95}semigroup :~'a monoid -> 'a semigroup\\
+\hspace*{0pt} ~val semigroup{\char95}monoid :~'a monoid -> 'a semigroup\\
 \hspace*{0pt} ~val neutral :~'a monoid -> 'a\\
 \hspace*{0pt} ~val pow :~'a monoid -> nat -> 'a -> 'a\\
 \hspace*{0pt} ~val plus{\char95}nat :~nat -> nat -> nat\\
@@ -358,12 +358,12 @@
 \hspace*{0pt}type 'a semigroup = {\char123}mult :~'a -> 'a -> 'a{\char125};\\
 \hspace*{0pt}val mult = {\char35}mult :~'a semigroup -> 'a -> 'a -> 'a;\\
 \hspace*{0pt}\\
-\hspace*{0pt}type 'a monoid = {\char123}monoid{\char95}semigroup :~'a semigroup,~neutral :~'a{\char125};\\
-\hspace*{0pt}val monoid{\char95}semigroup = {\char35}monoid{\char95}semigroup :~'a monoid -> 'a semigroup;\\
+\hspace*{0pt}type 'a monoid = {\char123}semigroup{\char95}monoid :~'a semigroup,~neutral :~'a{\char125};\\
+\hspace*{0pt}val semigroup{\char95}monoid = {\char35}semigroup{\char95}monoid :~'a monoid -> 'a semigroup;\\
 \hspace*{0pt}val neutral = {\char35}neutral :~'a monoid -> 'a;\\
 \hspace*{0pt}\\
 \hspace*{0pt}fun pow A{\char95}~Zero{\char95}nat a = neutral A{\char95}\\
-\hspace*{0pt} ~| pow A{\char95}~(Suc n) a = mult (monoid{\char95}semigroup A{\char95}) a (pow A{\char95}~n a);\\
+\hspace*{0pt} ~| pow A{\char95}~(Suc n) a = mult (semigroup{\char95}monoid A{\char95}) a (pow A{\char95}~n a);\\
 \hspace*{0pt}\\
 \hspace*{0pt}fun plus{\char95}nat (Suc m) n = plus{\char95}nat m (Suc n)\\
 \hspace*{0pt} ~| plus{\char95}nat Zero{\char95}nat n = n;\\
@@ -375,7 +375,7 @@
 \hspace*{0pt}\\
 \hspace*{0pt}val semigroup{\char95}nat = {\char123}mult = mult{\char95}nat{\char125}~:~nat semigroup;\\
 \hspace*{0pt}\\
-\hspace*{0pt}val monoid{\char95}nat = {\char123}monoid{\char95}semigroup = semigroup{\char95}nat,~neutral = neutral{\char95}nat{\char125}\\
+\hspace*{0pt}val monoid{\char95}nat = {\char123}semigroup{\char95}monoid = semigroup{\char95}nat,~neutral = neutral{\char95}nat{\char125}\\
 \hspace*{0pt} ~:~nat monoid;\\
 \hspace*{0pt}\\
 \hspace*{0pt}fun bexp n = pow monoid{\char95}nat n (Suc (Suc Zero{\char95}nat));\\