--- a/doc-src/AxClass/generated/Group.tex Mon Aug 21 18:49:38 2000 +0200
+++ b/doc-src/AxClass/generated/Group.tex Mon Aug 21 19:03:58 2000 +0200
@@ -1,7 +1,7 @@
\begin{isabelle}%
%
\isamarkupheader{Basic group theory}
-\isacommand{theory}\ Group\ =\ Main:%
+\isacommand{theory}\ Group\ {\isacharequal}\ Main{\isacharcolon}%
\begin{isamarkuptext}%
\medskip\noindent The meta-type system of Isabelle supports
\emph{intersections} and \emph{inclusions} of type classes. These
@@ -19,9 +19,9 @@
signature parts of our structures.%
\end{isamarkuptext}%
\isacommand{consts}\isanewline
-\ \ times\ ::\ {\isachardoublequote}{\isacharprime}a\ ={\isachargreater}\ {\isacharprime}a\ ={\isachargreater}\ {\isacharprime}a{\isachardoublequote}\ \ \ \ {\isacharparenleft}\isakeyword{infixl}\ {\isachardoublequote}{\isasymOtimes}{\isachardoublequote}\ 70{\isacharparenright}\isanewline
-\ \ inverse\ ::\ {\isachardoublequote}{\isacharprime}a\ ={\isachargreater}\ {\isacharprime}a{\isachardoublequote}\ \ \ \ \ \ \ \ {\isacharparenleft}{\isachardoublequote}{\isacharparenleft}{\isacharunderscore}{\isasyminv}{\isacharparenright}{\isachardoublequote}\ {\isacharbrackleft}1000{\isacharbrackright}\ 999{\isacharparenright}\isanewline
-\ \ one\ ::\ {\isacharprime}a\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ {\isacharparenleft}{\isachardoublequote}{\isasymunit}{\isachardoublequote}{\isacharparenright}%
+\ \ times\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequote}{\isacharprime}a\ {\isacharequal}{\isachargreater}\ {\isacharprime}a\ {\isacharequal}{\isachargreater}\ {\isacharprime}a{\isachardoublequote}\ \ \ \ {\isacharparenleft}\isakeyword{infixl}\ {\isachardoublequote}{\isasymOtimes}{\isachardoublequote}\ \isadigit{7}\isadigit{0}{\isacharparenright}\isanewline
+\ \ inverse\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequote}{\isacharprime}a\ {\isacharequal}{\isachargreater}\ {\isacharprime}a{\isachardoublequote}\ \ \ \ \ \ \ \ {\isacharparenleft}{\isachardoublequote}{\isacharparenleft}{\isacharunderscore}{\isasyminv}{\isacharparenright}{\isachardoublequote}\ {\isacharbrackleft}\isadigit{1}\isadigit{0}\isadigit{0}\isadigit{0}{\isacharbrackright}\ \isadigit{9}\isadigit{9}\isadigit{9}{\isacharparenright}\isanewline
+\ \ one\ {\isacharcolon}{\isacharcolon}\ {\isacharprime}a\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ {\isacharparenleft}{\isachardoublequote}{\isasymunit}{\isachardoublequote}{\isacharparenright}%
\begin{isamarkuptext}%
\noindent Next we define class $monoid$ of monoids with operations
$\TIMES$ and $1$. Note that multiple class axioms are allowed for
@@ -30,9 +30,9 @@
\end{isamarkuptext}%
\isacommand{axclass}\isanewline
\ \ monoid\ {\isacharless}\ {\isachardoublequote}term{\isachardoublequote}\isanewline
-\ \ assoc:\ \ \ \ \ \ {\isachardoublequote}{\isacharparenleft}x\ {\isasymOtimes}\ y{\isacharparenright}\ {\isasymOtimes}\ z\ =\ x\ {\isasymOtimes}\ {\isacharparenleft}y\ {\isasymOtimes}\ z{\isacharparenright}{\isachardoublequote}\isanewline
-\ \ left{\isacharunderscore}unit:\ \ {\isachardoublequote}{\isasymunit}\ {\isasymOtimes}\ x\ =\ x{\isachardoublequote}\isanewline
-\ \ right{\isacharunderscore}unit:\ {\isachardoublequote}x\ {\isasymOtimes}\ {\isasymunit}\ =\ x{\isachardoublequote}%
+\ \ assoc{\isacharcolon}\ \ \ \ \ \ {\isachardoublequote}{\isacharparenleft}x\ {\isasymOtimes}\ y{\isacharparenright}\ {\isasymOtimes}\ z\ {\isacharequal}\ x\ {\isasymOtimes}\ {\isacharparenleft}y\ {\isasymOtimes}\ z{\isacharparenright}{\isachardoublequote}\isanewline
+\ \ left{\isacharunderscore}unit{\isacharcolon}\ \ {\isachardoublequote}{\isasymunit}\ {\isasymOtimes}\ x\ {\isacharequal}\ x{\isachardoublequote}\isanewline
+\ \ right{\isacharunderscore}unit{\isacharcolon}\ {\isachardoublequote}x\ {\isasymOtimes}\ {\isasymunit}\ {\isacharequal}\ x{\isachardoublequote}%
\begin{isamarkuptext}%
\noindent So class $monoid$ contains exactly those types $\tau$ where
$\TIMES :: \tau \To \tau \To \tau$ and $1 :: \tau$ are specified
@@ -48,16 +48,16 @@
\end{isamarkuptext}%
\isacommand{axclass}\isanewline
\ \ semigroup\ {\isacharless}\ {\isachardoublequote}term{\isachardoublequote}\isanewline
-\ \ assoc:\ {\isachardoublequote}{\isacharparenleft}x\ {\isasymOtimes}\ y{\isacharparenright}\ {\isasymOtimes}\ z\ =\ x\ {\isasymOtimes}\ {\isacharparenleft}y\ {\isasymOtimes}\ z{\isacharparenright}{\isachardoublequote}\isanewline
+\ \ assoc{\isacharcolon}\ {\isachardoublequote}{\isacharparenleft}x\ {\isasymOtimes}\ y{\isacharparenright}\ {\isasymOtimes}\ z\ {\isacharequal}\ x\ {\isasymOtimes}\ {\isacharparenleft}y\ {\isasymOtimes}\ z{\isacharparenright}{\isachardoublequote}\isanewline
\isanewline
\isacommand{axclass}\isanewline
\ \ group\ {\isacharless}\ semigroup\isanewline
-\ \ left{\isacharunderscore}unit:\ \ \ \ {\isachardoublequote}{\isasymunit}\ {\isasymOtimes}\ x\ =\ x{\isachardoublequote}\isanewline
-\ \ left{\isacharunderscore}inverse:\ {\isachardoublequote}x{\isasyminv}\ {\isasymOtimes}\ x\ =\ {\isasymunit}{\isachardoublequote}\isanewline
+\ \ left{\isacharunderscore}unit{\isacharcolon}\ \ \ \ {\isachardoublequote}{\isasymunit}\ {\isasymOtimes}\ x\ {\isacharequal}\ x{\isachardoublequote}\isanewline
+\ \ left{\isacharunderscore}inverse{\isacharcolon}\ {\isachardoublequote}x{\isasyminv}\ {\isasymOtimes}\ x\ {\isacharequal}\ {\isasymunit}{\isachardoublequote}\isanewline
\isanewline
\isacommand{axclass}\isanewline
\ \ agroup\ {\isacharless}\ group\isanewline
-\ \ commute:\ {\isachardoublequote}x\ {\isasymOtimes}\ y\ =\ y\ {\isasymOtimes}\ x{\isachardoublequote}%
+\ \ commute{\isacharcolon}\ {\isachardoublequote}x\ {\isasymOtimes}\ y\ {\isacharequal}\ y\ {\isasymOtimes}\ x{\isachardoublequote}%
\begin{isamarkuptext}%
\noindent Class $group$ inherits associativity of $\TIMES$ from
$semigroup$ and adds two further group axioms. Similarly, $agroup$
@@ -85,42 +85,42 @@
``abstract theorems''. For example, we may now derive the following
well-known laws of general groups.%
\end{isamarkuptext}%
-\isacommand{theorem}\ group{\isacharunderscore}right{\isacharunderscore}inverse:\ {\isachardoublequote}x\ {\isasymOtimes}\ x{\isasyminv}\ =\ {\isacharparenleft}{\isasymunit}{\isasymColon}{\isacharprime}a{\isasymColon}group{\isacharparenright}{\isachardoublequote}\isanewline
+\isacommand{theorem}\ group{\isacharunderscore}right{\isacharunderscore}inverse{\isacharcolon}\ {\isachardoublequote}x\ {\isasymOtimes}\ x{\isasyminv}\ {\isacharequal}\ {\isacharparenleft}{\isasymunit}{\isasymColon}{\isacharprime}a{\isasymColon}group{\isacharparenright}{\isachardoublequote}\isanewline
\isacommand{proof}\ {\isacharminus}\isanewline
-\ \ \isacommand{have}\ {\isachardoublequote}x\ {\isasymOtimes}\ x{\isasyminv}\ =\ {\isasymunit}\ {\isasymOtimes}\ {\isacharparenleft}x\ {\isasymOtimes}\ x{\isasyminv}{\isacharparenright}{\isachardoublequote}\isanewline
-\ \ \ \ \isacommand{by}\ {\isacharparenleft}simp\ only:\ group.left{\isacharunderscore}unit{\isacharparenright}\isanewline
-\ \ \isacommand{also}\ \isacommand{have}\ {\isachardoublequote}...\ =\ {\isasymunit}\ {\isasymOtimes}\ x\ {\isasymOtimes}\ x{\isasyminv}{\isachardoublequote}\isanewline
-\ \ \ \ \isacommand{by}\ {\isacharparenleft}simp\ only:\ semigroup.assoc{\isacharparenright}\isanewline
-\ \ \isacommand{also}\ \isacommand{have}\ {\isachardoublequote}...\ =\ {\isacharparenleft}x{\isasyminv}{\isacharparenright}{\isasyminv}\ {\isasymOtimes}\ x{\isasyminv}\ {\isasymOtimes}\ x\ {\isasymOtimes}\ x{\isasyminv}{\isachardoublequote}\isanewline
-\ \ \ \ \isacommand{by}\ {\isacharparenleft}simp\ only:\ group.left{\isacharunderscore}inverse{\isacharparenright}\isanewline
-\ \ \isacommand{also}\ \isacommand{have}\ {\isachardoublequote}...\ =\ {\isacharparenleft}x{\isasyminv}{\isacharparenright}{\isasyminv}\ {\isasymOtimes}\ {\isacharparenleft}x{\isasyminv}\ {\isasymOtimes}\ x{\isacharparenright}\ {\isasymOtimes}\ x{\isasyminv}{\isachardoublequote}\isanewline
-\ \ \ \ \isacommand{by}\ {\isacharparenleft}simp\ only:\ semigroup.assoc{\isacharparenright}\isanewline
-\ \ \isacommand{also}\ \isacommand{have}\ {\isachardoublequote}...\ =\ {\isacharparenleft}x{\isasyminv}{\isacharparenright}{\isasyminv}\ {\isasymOtimes}\ {\isasymunit}\ {\isasymOtimes}\ x{\isasyminv}{\isachardoublequote}\isanewline
-\ \ \ \ \isacommand{by}\ {\isacharparenleft}simp\ only:\ group.left{\isacharunderscore}inverse{\isacharparenright}\isanewline
-\ \ \isacommand{also}\ \isacommand{have}\ {\isachardoublequote}...\ =\ {\isacharparenleft}x{\isasyminv}{\isacharparenright}{\isasyminv}\ {\isasymOtimes}\ {\isacharparenleft}{\isasymunit}\ {\isasymOtimes}\ x{\isasyminv}{\isacharparenright}{\isachardoublequote}\isanewline
-\ \ \ \ \isacommand{by}\ {\isacharparenleft}simp\ only:\ semigroup.assoc{\isacharparenright}\isanewline
-\ \ \isacommand{also}\ \isacommand{have}\ {\isachardoublequote}...\ =\ {\isacharparenleft}x{\isasyminv}{\isacharparenright}{\isasyminv}\ {\isasymOtimes}\ x{\isasyminv}{\isachardoublequote}\isanewline
-\ \ \ \ \isacommand{by}\ {\isacharparenleft}simp\ only:\ group.left{\isacharunderscore}unit{\isacharparenright}\isanewline
-\ \ \isacommand{also}\ \isacommand{have}\ {\isachardoublequote}...\ =\ {\isasymunit}{\isachardoublequote}\isanewline
-\ \ \ \ \isacommand{by}\ {\isacharparenleft}simp\ only:\ group.left{\isacharunderscore}inverse{\isacharparenright}\isanewline
-\ \ \isacommand{finally}\ \isacommand{show}\ ?thesis\ \isacommand{.}\isanewline
+\ \ \isacommand{have}\ {\isachardoublequote}x\ {\isasymOtimes}\ x{\isasyminv}\ {\isacharequal}\ {\isasymunit}\ {\isasymOtimes}\ {\isacharparenleft}x\ {\isasymOtimes}\ x{\isasyminv}{\isacharparenright}{\isachardoublequote}\isanewline
+\ \ \ \ \isacommand{by}\ {\isacharparenleft}simp\ only{\isacharcolon}\ group{\isachardot}left{\isacharunderscore}unit{\isacharparenright}\isanewline
+\ \ \isacommand{also}\ \isacommand{have}\ {\isachardoublequote}{\isachardot}{\isachardot}{\isachardot}\ {\isacharequal}\ {\isasymunit}\ {\isasymOtimes}\ x\ {\isasymOtimes}\ x{\isasyminv}{\isachardoublequote}\isanewline
+\ \ \ \ \isacommand{by}\ {\isacharparenleft}simp\ only{\isacharcolon}\ semigroup{\isachardot}assoc{\isacharparenright}\isanewline
+\ \ \isacommand{also}\ \isacommand{have}\ {\isachardoublequote}{\isachardot}{\isachardot}{\isachardot}\ {\isacharequal}\ {\isacharparenleft}x{\isasyminv}{\isacharparenright}{\isasyminv}\ {\isasymOtimes}\ x{\isasyminv}\ {\isasymOtimes}\ x\ {\isasymOtimes}\ x{\isasyminv}{\isachardoublequote}\isanewline
+\ \ \ \ \isacommand{by}\ {\isacharparenleft}simp\ only{\isacharcolon}\ group{\isachardot}left{\isacharunderscore}inverse{\isacharparenright}\isanewline
+\ \ \isacommand{also}\ \isacommand{have}\ {\isachardoublequote}{\isachardot}{\isachardot}{\isachardot}\ {\isacharequal}\ {\isacharparenleft}x{\isasyminv}{\isacharparenright}{\isasyminv}\ {\isasymOtimes}\ {\isacharparenleft}x{\isasyminv}\ {\isasymOtimes}\ x{\isacharparenright}\ {\isasymOtimes}\ x{\isasyminv}{\isachardoublequote}\isanewline
+\ \ \ \ \isacommand{by}\ {\isacharparenleft}simp\ only{\isacharcolon}\ semigroup{\isachardot}assoc{\isacharparenright}\isanewline
+\ \ \isacommand{also}\ \isacommand{have}\ {\isachardoublequote}{\isachardot}{\isachardot}{\isachardot}\ {\isacharequal}\ {\isacharparenleft}x{\isasyminv}{\isacharparenright}{\isasyminv}\ {\isasymOtimes}\ {\isasymunit}\ {\isasymOtimes}\ x{\isasyminv}{\isachardoublequote}\isanewline
+\ \ \ \ \isacommand{by}\ {\isacharparenleft}simp\ only{\isacharcolon}\ group{\isachardot}left{\isacharunderscore}inverse{\isacharparenright}\isanewline
+\ \ \isacommand{also}\ \isacommand{have}\ {\isachardoublequote}{\isachardot}{\isachardot}{\isachardot}\ {\isacharequal}\ {\isacharparenleft}x{\isasyminv}{\isacharparenright}{\isasyminv}\ {\isasymOtimes}\ {\isacharparenleft}{\isasymunit}\ {\isasymOtimes}\ x{\isasyminv}{\isacharparenright}{\isachardoublequote}\isanewline
+\ \ \ \ \isacommand{by}\ {\isacharparenleft}simp\ only{\isacharcolon}\ semigroup{\isachardot}assoc{\isacharparenright}\isanewline
+\ \ \isacommand{also}\ \isacommand{have}\ {\isachardoublequote}{\isachardot}{\isachardot}{\isachardot}\ {\isacharequal}\ {\isacharparenleft}x{\isasyminv}{\isacharparenright}{\isasyminv}\ {\isasymOtimes}\ x{\isasyminv}{\isachardoublequote}\isanewline
+\ \ \ \ \isacommand{by}\ {\isacharparenleft}simp\ only{\isacharcolon}\ group{\isachardot}left{\isacharunderscore}unit{\isacharparenright}\isanewline
+\ \ \isacommand{also}\ \isacommand{have}\ {\isachardoublequote}{\isachardot}{\isachardot}{\isachardot}\ {\isacharequal}\ {\isasymunit}{\isachardoublequote}\isanewline
+\ \ \ \ \isacommand{by}\ {\isacharparenleft}simp\ only{\isacharcolon}\ group{\isachardot}left{\isacharunderscore}inverse{\isacharparenright}\isanewline
+\ \ \isacommand{finally}\ \isacommand{show}\ {\isacharquery}thesis\ \isacommand{{\isachardot}}\isanewline
\isacommand{qed}%
\begin{isamarkuptext}%
\noindent With $group_right_inverse$ already available,
$group_right_unit$\label{thm:group-right-unit} is now established
much easier.%
\end{isamarkuptext}%
-\isacommand{theorem}\ group{\isacharunderscore}right{\isacharunderscore}unit:\ {\isachardoublequote}x\ {\isasymOtimes}\ {\isasymunit}\ =\ {\isacharparenleft}x{\isasymColon}{\isacharprime}a{\isasymColon}group{\isacharparenright}{\isachardoublequote}\isanewline
+\isacommand{theorem}\ group{\isacharunderscore}right{\isacharunderscore}unit{\isacharcolon}\ {\isachardoublequote}x\ {\isasymOtimes}\ {\isasymunit}\ {\isacharequal}\ {\isacharparenleft}x{\isasymColon}{\isacharprime}a{\isasymColon}group{\isacharparenright}{\isachardoublequote}\isanewline
\isacommand{proof}\ {\isacharminus}\isanewline
-\ \ \isacommand{have}\ {\isachardoublequote}x\ {\isasymOtimes}\ {\isasymunit}\ =\ x\ {\isasymOtimes}\ {\isacharparenleft}x{\isasyminv}\ {\isasymOtimes}\ x{\isacharparenright}{\isachardoublequote}\isanewline
-\ \ \ \ \isacommand{by}\ {\isacharparenleft}simp\ only:\ group.left{\isacharunderscore}inverse{\isacharparenright}\isanewline
-\ \ \isacommand{also}\ \isacommand{have}\ {\isachardoublequote}...\ =\ x\ {\isasymOtimes}\ x{\isasyminv}\ {\isasymOtimes}\ x{\isachardoublequote}\isanewline
-\ \ \ \ \isacommand{by}\ {\isacharparenleft}simp\ only:\ semigroup.assoc{\isacharparenright}\isanewline
-\ \ \isacommand{also}\ \isacommand{have}\ {\isachardoublequote}...\ =\ {\isasymunit}\ {\isasymOtimes}\ x{\isachardoublequote}\isanewline
-\ \ \ \ \isacommand{by}\ {\isacharparenleft}simp\ only:\ group{\isacharunderscore}right{\isacharunderscore}inverse{\isacharparenright}\isanewline
-\ \ \isacommand{also}\ \isacommand{have}\ {\isachardoublequote}...\ =\ x{\isachardoublequote}\isanewline
-\ \ \ \ \isacommand{by}\ {\isacharparenleft}simp\ only:\ group.left{\isacharunderscore}unit{\isacharparenright}\isanewline
-\ \ \isacommand{finally}\ \isacommand{show}\ ?thesis\ \isacommand{.}\isanewline
+\ \ \isacommand{have}\ {\isachardoublequote}x\ {\isasymOtimes}\ {\isasymunit}\ {\isacharequal}\ x\ {\isasymOtimes}\ {\isacharparenleft}x{\isasyminv}\ {\isasymOtimes}\ x{\isacharparenright}{\isachardoublequote}\isanewline
+\ \ \ \ \isacommand{by}\ {\isacharparenleft}simp\ only{\isacharcolon}\ group{\isachardot}left{\isacharunderscore}inverse{\isacharparenright}\isanewline
+\ \ \isacommand{also}\ \isacommand{have}\ {\isachardoublequote}{\isachardot}{\isachardot}{\isachardot}\ {\isacharequal}\ x\ {\isasymOtimes}\ x{\isasyminv}\ {\isasymOtimes}\ x{\isachardoublequote}\isanewline
+\ \ \ \ \isacommand{by}\ {\isacharparenleft}simp\ only{\isacharcolon}\ semigroup{\isachardot}assoc{\isacharparenright}\isanewline
+\ \ \isacommand{also}\ \isacommand{have}\ {\isachardoublequote}{\isachardot}{\isachardot}{\isachardot}\ {\isacharequal}\ {\isasymunit}\ {\isasymOtimes}\ x{\isachardoublequote}\isanewline
+\ \ \ \ \isacommand{by}\ {\isacharparenleft}simp\ only{\isacharcolon}\ group{\isacharunderscore}right{\isacharunderscore}inverse{\isacharparenright}\isanewline
+\ \ \isacommand{also}\ \isacommand{have}\ {\isachardoublequote}{\isachardot}{\isachardot}{\isachardot}\ {\isacharequal}\ x{\isachardoublequote}\isanewline
+\ \ \ \ \isacommand{by}\ {\isacharparenleft}simp\ only{\isacharcolon}\ group{\isachardot}left{\isacharunderscore}unit{\isacharparenright}\isanewline
+\ \ \isacommand{finally}\ \isacommand{show}\ {\isacharquery}thesis\ \isacommand{{\isachardot}}\isanewline
\isacommand{qed}%
\begin{isamarkuptext}%
\medskip Abstract theorems may be instantiated to only those types
@@ -171,19 +171,19 @@
\end{isamarkuptext}%
\isacommand{instance}\ monoid\ {\isacharless}\ semigroup\isanewline
\isacommand{proof}\ intro{\isacharunderscore}classes\isanewline
-\ \ \isacommand{fix}\ x\ y\ z\ ::\ {\isachardoublequote}{\isacharprime}a{\isasymColon}monoid{\isachardoublequote}\isanewline
-\ \ \isacommand{show}\ {\isachardoublequote}x\ {\isasymOtimes}\ y\ {\isasymOtimes}\ z\ =\ x\ {\isasymOtimes}\ {\isacharparenleft}y\ {\isasymOtimes}\ z{\isacharparenright}{\isachardoublequote}\isanewline
-\ \ \ \ \isacommand{by}\ {\isacharparenleft}rule\ monoid.assoc{\isacharparenright}\isanewline
+\ \ \isacommand{fix}\ x\ y\ z\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequote}{\isacharprime}a{\isasymColon}monoid{\isachardoublequote}\isanewline
+\ \ \isacommand{show}\ {\isachardoublequote}x\ {\isasymOtimes}\ y\ {\isasymOtimes}\ z\ {\isacharequal}\ x\ {\isasymOtimes}\ {\isacharparenleft}y\ {\isasymOtimes}\ z{\isacharparenright}{\isachardoublequote}\isanewline
+\ \ \ \ \isacommand{by}\ {\isacharparenleft}rule\ monoid{\isachardot}assoc{\isacharparenright}\isanewline
\isacommand{qed}\isanewline
\isanewline
\isacommand{instance}\ group\ {\isacharless}\ monoid\isanewline
\isacommand{proof}\ intro{\isacharunderscore}classes\isanewline
-\ \ \isacommand{fix}\ x\ y\ z\ ::\ {\isachardoublequote}{\isacharprime}a{\isasymColon}group{\isachardoublequote}\isanewline
-\ \ \isacommand{show}\ {\isachardoublequote}x\ {\isasymOtimes}\ y\ {\isasymOtimes}\ z\ =\ x\ {\isasymOtimes}\ {\isacharparenleft}y\ {\isasymOtimes}\ z{\isacharparenright}{\isachardoublequote}\isanewline
-\ \ \ \ \isacommand{by}\ {\isacharparenleft}rule\ semigroup.assoc{\isacharparenright}\isanewline
-\ \ \isacommand{show}\ {\isachardoublequote}{\isasymunit}\ {\isasymOtimes}\ x\ =\ x{\isachardoublequote}\isanewline
-\ \ \ \ \isacommand{by}\ {\isacharparenleft}rule\ group.left{\isacharunderscore}unit{\isacharparenright}\isanewline
-\ \ \isacommand{show}\ {\isachardoublequote}x\ {\isasymOtimes}\ {\isasymunit}\ =\ x{\isachardoublequote}\isanewline
+\ \ \isacommand{fix}\ x\ y\ z\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequote}{\isacharprime}a{\isasymColon}group{\isachardoublequote}\isanewline
+\ \ \isacommand{show}\ {\isachardoublequote}x\ {\isasymOtimes}\ y\ {\isasymOtimes}\ z\ {\isacharequal}\ x\ {\isasymOtimes}\ {\isacharparenleft}y\ {\isasymOtimes}\ z{\isacharparenright}{\isachardoublequote}\isanewline
+\ \ \ \ \isacommand{by}\ {\isacharparenleft}rule\ semigroup{\isachardot}assoc{\isacharparenright}\isanewline
+\ \ \isacommand{show}\ {\isachardoublequote}{\isasymunit}\ {\isasymOtimes}\ x\ {\isacharequal}\ x{\isachardoublequote}\isanewline
+\ \ \ \ \isacommand{by}\ {\isacharparenleft}rule\ group{\isachardot}left{\isacharunderscore}unit{\isacharparenright}\isanewline
+\ \ \isacommand{show}\ {\isachardoublequote}x\ {\isasymOtimes}\ {\isasymunit}\ {\isacharequal}\ x{\isachardoublequote}\isanewline
\ \ \ \ \isacommand{by}\ {\isacharparenleft}rule\ group{\isacharunderscore}right{\isacharunderscore}unit{\isacharparenright}\isanewline
\isacommand{qed}%
\begin{isamarkuptext}%
@@ -215,9 +215,9 @@
$False$ as $1$ forms an Abelian group.%
\end{isamarkuptext}%
\isacommand{defs}\ {\isacharparenleft}\isakeyword{overloaded}{\isacharparenright}\isanewline
-\ \ times{\isacharunderscore}bool{\isacharunderscore}def:\ \ \ {\isachardoublequote}x\ {\isasymOtimes}\ y\ {\isasymequiv}\ x\ {\isasymnoteq}\ {\isacharparenleft}y{\isasymColon}bool{\isacharparenright}{\isachardoublequote}\isanewline
-\ \ inverse{\isacharunderscore}bool{\isacharunderscore}def:\ {\isachardoublequote}x{\isasyminv}\ {\isasymequiv}\ x{\isasymColon}bool{\isachardoublequote}\isanewline
-\ \ unit{\isacharunderscore}bool{\isacharunderscore}def:\ \ \ \ {\isachardoublequote}{\isasymunit}\ {\isasymequiv}\ False{\isachardoublequote}%
+\ \ times{\isacharunderscore}bool{\isacharunderscore}def{\isacharcolon}\ \ \ {\isachardoublequote}x\ {\isasymOtimes}\ y\ {\isasymequiv}\ x\ {\isasymnoteq}\ {\isacharparenleft}y{\isasymColon}bool{\isacharparenright}{\isachardoublequote}\isanewline
+\ \ inverse{\isacharunderscore}bool{\isacharunderscore}def{\isacharcolon}\ {\isachardoublequote}x{\isasyminv}\ {\isasymequiv}\ x{\isasymColon}bool{\isachardoublequote}\isanewline
+\ \ unit{\isacharunderscore}bool{\isacharunderscore}def{\isacharcolon}\ \ \ \ {\isachardoublequote}{\isasymunit}\ {\isasymequiv}\ False{\isachardoublequote}%
\begin{isamarkuptext}%
\medskip It is important to note that above $\DEFS$ are just
overloaded meta-level constant definitions, where type classes are
@@ -232,14 +232,14 @@
operations on type $bool$ appropriately, the class membership $bool
:: agroup$ may be now derived as follows.%
\end{isamarkuptext}%
-\isacommand{instance}\ bool\ ::\ agroup\isanewline
-\isacommand{proof}\ {\isacharparenleft}intro{\isacharunderscore}classes,\isanewline
+\isacommand{instance}\ bool\ {\isacharcolon}{\isacharcolon}\ agroup\isanewline
+\isacommand{proof}\ {\isacharparenleft}intro{\isacharunderscore}classes{\isacharcomma}\isanewline
\ \ \ \ unfold\ times{\isacharunderscore}bool{\isacharunderscore}def\ inverse{\isacharunderscore}bool{\isacharunderscore}def\ unit{\isacharunderscore}bool{\isacharunderscore}def{\isacharparenright}\isanewline
\ \ \isacommand{fix}\ x\ y\ z\isanewline
-\ \ \isacommand{show}\ {\isachardoublequote}{\isacharparenleft}{\isacharparenleft}x\ {\isasymnoteq}\ y{\isacharparenright}\ {\isasymnoteq}\ z{\isacharparenright}\ =\ {\isacharparenleft}x\ {\isasymnoteq}\ {\isacharparenleft}y\ {\isasymnoteq}\ z{\isacharparenright}{\isacharparenright}{\isachardoublequote}\ \isacommand{by}\ blast\isanewline
-\ \ \isacommand{show}\ {\isachardoublequote}{\isacharparenleft}False\ {\isasymnoteq}\ x{\isacharparenright}\ =\ x{\isachardoublequote}\ \isacommand{by}\ blast\isanewline
-\ \ \isacommand{show}\ {\isachardoublequote}{\isacharparenleft}x\ {\isasymnoteq}\ x{\isacharparenright}\ =\ False{\isachardoublequote}\ \isacommand{by}\ blast\isanewline
-\ \ \isacommand{show}\ {\isachardoublequote}{\isacharparenleft}x\ {\isasymnoteq}\ y{\isacharparenright}\ =\ {\isacharparenleft}y\ {\isasymnoteq}\ x{\isacharparenright}{\isachardoublequote}\ \isacommand{by}\ blast\isanewline
+\ \ \isacommand{show}\ {\isachardoublequote}{\isacharparenleft}{\isacharparenleft}x\ {\isasymnoteq}\ y{\isacharparenright}\ {\isasymnoteq}\ z{\isacharparenright}\ {\isacharequal}\ {\isacharparenleft}x\ {\isasymnoteq}\ {\isacharparenleft}y\ {\isasymnoteq}\ z{\isacharparenright}{\isacharparenright}{\isachardoublequote}\ \isacommand{by}\ blast\isanewline
+\ \ \isacommand{show}\ {\isachardoublequote}{\isacharparenleft}False\ {\isasymnoteq}\ x{\isacharparenright}\ {\isacharequal}\ x{\isachardoublequote}\ \isacommand{by}\ blast\isanewline
+\ \ \isacommand{show}\ {\isachardoublequote}{\isacharparenleft}x\ {\isasymnoteq}\ x{\isacharparenright}\ {\isacharequal}\ False{\isachardoublequote}\ \isacommand{by}\ blast\isanewline
+\ \ \isacommand{show}\ {\isachardoublequote}{\isacharparenleft}x\ {\isasymnoteq}\ y{\isacharparenright}\ {\isacharequal}\ {\isacharparenleft}y\ {\isasymnoteq}\ x{\isacharparenright}{\isachardoublequote}\ \isacommand{by}\ blast\isanewline
\isacommand{qed}%
\begin{isamarkuptext}%
The result of an $\isakeyword{instance}$ statement is both expressed
@@ -270,22 +270,22 @@
$\TIMES$ component-wise to binary products $\alpha \times \beta$.%
\end{isamarkuptext}%
\isacommand{defs}\ {\isacharparenleft}\isakeyword{overloaded}{\isacharparenright}\isanewline
-\ \ times{\isacharunderscore}prod{\isacharunderscore}def:\ {\isachardoublequote}p\ {\isasymOtimes}\ q\ {\isasymequiv}\ {\isacharparenleft}fst\ p\ {\isasymOtimes}\ fst\ q,\ snd\ p\ {\isasymOtimes}\ snd\ q{\isacharparenright}{\isachardoublequote}%
+\ \ times{\isacharunderscore}prod{\isacharunderscore}def{\isacharcolon}\ {\isachardoublequote}p\ {\isasymOtimes}\ q\ {\isasymequiv}\ {\isacharparenleft}fst\ p\ {\isasymOtimes}\ fst\ q{\isacharcomma}\ snd\ p\ {\isasymOtimes}\ snd\ q{\isacharparenright}{\isachardoublequote}%
\begin{isamarkuptext}%
It is very easy to see that associativity of $\TIMES^\alpha$ and
$\TIMES^\beta$ transfers to ${\TIMES}^{\alpha \times \beta}$. Hence
the binary type constructor $\times$ maps semigroups to semigroups.
This may be established formally as follows.%
\end{isamarkuptext}%
-\isacommand{instance}\ {\isacharasterisk}\ ::\ {\isacharparenleft}semigroup,\ semigroup{\isacharparenright}\ semigroup\isanewline
-\isacommand{proof}\ {\isacharparenleft}intro{\isacharunderscore}classes,\ unfold\ times{\isacharunderscore}prod{\isacharunderscore}def{\isacharparenright}\isanewline
-\ \ \isacommand{fix}\ p\ q\ r\ ::\ {\isachardoublequote}{\isacharprime}a{\isasymColon}semigroup\ {\isasymtimes}\ {\isacharprime}b{\isasymColon}semigroup{\isachardoublequote}\isanewline
+\isacommand{instance}\ {\isacharasterisk}\ {\isacharcolon}{\isacharcolon}\ {\isacharparenleft}semigroup{\isacharcomma}\ semigroup{\isacharparenright}\ semigroup\isanewline
+\isacommand{proof}\ {\isacharparenleft}intro{\isacharunderscore}classes{\isacharcomma}\ unfold\ times{\isacharunderscore}prod{\isacharunderscore}def{\isacharparenright}\isanewline
+\ \ \isacommand{fix}\ p\ q\ r\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequote}{\isacharprime}a{\isasymColon}semigroup\ {\isasymtimes}\ {\isacharprime}b{\isasymColon}semigroup{\isachardoublequote}\isanewline
\ \ \isacommand{show}\isanewline
-\ \ \ \ {\isachardoublequote}{\isacharparenleft}fst\ {\isacharparenleft}fst\ p\ {\isasymOtimes}\ fst\ q,\ snd\ p\ {\isasymOtimes}\ snd\ q{\isacharparenright}\ {\isasymOtimes}\ fst\ r,\isanewline
-\ \ \ \ \ \ snd\ {\isacharparenleft}fst\ p\ {\isasymOtimes}\ fst\ q,\ snd\ p\ {\isasymOtimes}\ snd\ q{\isacharparenright}\ {\isasymOtimes}\ snd\ r{\isacharparenright}\ =\isanewline
-\ \ \ \ \ \ \ {\isacharparenleft}fst\ p\ {\isasymOtimes}\ fst\ {\isacharparenleft}fst\ q\ {\isasymOtimes}\ fst\ r,\ snd\ q\ {\isasymOtimes}\ snd\ r{\isacharparenright},\isanewline
-\ \ \ \ \ \ \ \ snd\ p\ {\isasymOtimes}\ snd\ {\isacharparenleft}fst\ q\ {\isasymOtimes}\ fst\ r,\ snd\ q\ {\isasymOtimes}\ snd\ r{\isacharparenright}{\isacharparenright}{\isachardoublequote}\isanewline
-\ \ \ \ \isacommand{by}\ {\isacharparenleft}simp\ add:\ semigroup.assoc{\isacharparenright}\isanewline
+\ \ \ \ {\isachardoublequote}{\isacharparenleft}fst\ {\isacharparenleft}fst\ p\ {\isasymOtimes}\ fst\ q{\isacharcomma}\ snd\ p\ {\isasymOtimes}\ snd\ q{\isacharparenright}\ {\isasymOtimes}\ fst\ r{\isacharcomma}\isanewline
+\ \ \ \ \ \ snd\ {\isacharparenleft}fst\ p\ {\isasymOtimes}\ fst\ q{\isacharcomma}\ snd\ p\ {\isasymOtimes}\ snd\ q{\isacharparenright}\ {\isasymOtimes}\ snd\ r{\isacharparenright}\ {\isacharequal}\isanewline
+\ \ \ \ \ \ \ {\isacharparenleft}fst\ p\ {\isasymOtimes}\ fst\ {\isacharparenleft}fst\ q\ {\isasymOtimes}\ fst\ r{\isacharcomma}\ snd\ q\ {\isasymOtimes}\ snd\ r{\isacharparenright}{\isacharcomma}\isanewline
+\ \ \ \ \ \ \ \ snd\ p\ {\isasymOtimes}\ snd\ {\isacharparenleft}fst\ q\ {\isasymOtimes}\ fst\ r{\isacharcomma}\ snd\ q\ {\isasymOtimes}\ snd\ r{\isacharparenright}{\isacharparenright}{\isachardoublequote}\isanewline
+\ \ \ \ \isacommand{by}\ {\isacharparenleft}simp\ add{\isacharcolon}\ semigroup{\isachardot}assoc{\isacharparenright}\isanewline
\isacommand{qed}%
\begin{isamarkuptext}%
Thus, if we view class instances as ``structures'', then overloaded
--- a/doc-src/AxClass/generated/NatClass.tex Mon Aug 21 18:49:38 2000 +0200
+++ b/doc-src/AxClass/generated/NatClass.tex Mon Aug 21 19:03:58 2000 +0200
@@ -1,7 +1,7 @@
\begin{isabelle}%
%
\isamarkupheader{Defining natural numbers in FOL \label{sec:ex-natclass}}
-\isacommand{theory}\ NatClass\ =\ FOL:%
+\isacommand{theory}\ NatClass\ {\isacharequal}\ FOL{\isacharcolon}%
\begin{isamarkuptext}%
\medskip\noindent Axiomatic type classes abstract over exactly one
type argument. Thus, any \emph{axiomatic} theory extension where each
@@ -13,21 +13,21 @@
\url{http://isabelle.in.tum.de/library/FOL/ex/NatClass.html}}%
\end{isamarkuptext}%
\isacommand{consts}\isanewline
-\ \ zero\ ::\ {\isacharprime}a\ \ \ \ {\isacharparenleft}{\isachardoublequote}0{\isachardoublequote}{\isacharparenright}\isanewline
-\ \ Suc\ ::\ {\isachardoublequote}{\isacharprime}a\ {\isasymRightarrow}\ {\isacharprime}a{\isachardoublequote}\isanewline
-\ \ rec\ ::\ {\isachardoublequote}{\isacharprime}a\ {\isasymRightarrow}\ {\isacharprime}a\ {\isasymRightarrow}\ {\isacharparenleft}{\isacharprime}a\ {\isasymRightarrow}\ {\isacharprime}a\ {\isasymRightarrow}\ {\isacharprime}a{\isacharparenright}\ {\isasymRightarrow}\ {\isacharprime}a{\isachardoublequote}\isanewline
+\ \ zero\ {\isacharcolon}{\isacharcolon}\ {\isacharprime}a\ \ \ \ {\isacharparenleft}{\isachardoublequote}\isadigit{0}{\isachardoublequote}{\isacharparenright}\isanewline
+\ \ Suc\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequote}{\isacharprime}a\ {\isasymRightarrow}\ {\isacharprime}a{\isachardoublequote}\isanewline
+\ \ rec\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequote}{\isacharprime}a\ {\isasymRightarrow}\ {\isacharprime}a\ {\isasymRightarrow}\ {\isacharparenleft}{\isacharprime}a\ {\isasymRightarrow}\ {\isacharprime}a\ {\isasymRightarrow}\ {\isacharprime}a{\isacharparenright}\ {\isasymRightarrow}\ {\isacharprime}a{\isachardoublequote}\isanewline
\isanewline
\isacommand{axclass}\isanewline
\ \ nat\ {\isacharless}\ {\isachardoublequote}term{\isachardoublequote}\isanewline
-\ \ induct:\ \ \ \ \ {\isachardoublequote}P{\isacharparenleft}0{\isacharparenright}\ {\isasymLongrightarrow}\ {\isacharparenleft}{\isasymAnd}x.\ P{\isacharparenleft}x{\isacharparenright}\ {\isasymLongrightarrow}\ P{\isacharparenleft}Suc{\isacharparenleft}x{\isacharparenright}{\isacharparenright}{\isacharparenright}\ {\isasymLongrightarrow}\ P{\isacharparenleft}n{\isacharparenright}{\isachardoublequote}\isanewline
-\ \ Suc{\isacharunderscore}inject:\ {\isachardoublequote}Suc{\isacharparenleft}m{\isacharparenright}\ =\ Suc{\isacharparenleft}n{\isacharparenright}\ {\isasymLongrightarrow}\ m\ =\ n{\isachardoublequote}\isanewline
-\ \ Suc{\isacharunderscore}neq{\isacharunderscore}0:\ \ {\isachardoublequote}Suc{\isacharparenleft}m{\isacharparenright}\ =\ 0\ {\isasymLongrightarrow}\ R{\isachardoublequote}\isanewline
-\ \ rec{\isacharunderscore}0:\ \ \ \ \ \ {\isachardoublequote}rec{\isacharparenleft}0,\ a,\ f{\isacharparenright}\ =\ a{\isachardoublequote}\isanewline
-\ \ rec{\isacharunderscore}Suc:\ \ \ \ {\isachardoublequote}rec{\isacharparenleft}Suc{\isacharparenleft}m{\isacharparenright},\ a,\ f{\isacharparenright}\ =\ f{\isacharparenleft}m,\ rec{\isacharparenleft}m,\ a,\ f{\isacharparenright}{\isacharparenright}{\isachardoublequote}\isanewline
+\ \ induct{\isacharcolon}\ \ \ \ \ {\isachardoublequote}P{\isacharparenleft}\isadigit{0}{\isacharparenright}\ {\isasymLongrightarrow}\ {\isacharparenleft}{\isasymAnd}x{\isachardot}\ P{\isacharparenleft}x{\isacharparenright}\ {\isasymLongrightarrow}\ P{\isacharparenleft}Suc{\isacharparenleft}x{\isacharparenright}{\isacharparenright}{\isacharparenright}\ {\isasymLongrightarrow}\ P{\isacharparenleft}n{\isacharparenright}{\isachardoublequote}\isanewline
+\ \ Suc{\isacharunderscore}inject{\isacharcolon}\ {\isachardoublequote}Suc{\isacharparenleft}m{\isacharparenright}\ {\isacharequal}\ Suc{\isacharparenleft}n{\isacharparenright}\ {\isasymLongrightarrow}\ m\ {\isacharequal}\ n{\isachardoublequote}\isanewline
+\ \ Suc{\isacharunderscore}neq{\isacharunderscore}\isadigit{0}{\isacharcolon}\ \ {\isachardoublequote}Suc{\isacharparenleft}m{\isacharparenright}\ {\isacharequal}\ \isadigit{0}\ {\isasymLongrightarrow}\ R{\isachardoublequote}\isanewline
+\ \ rec{\isacharunderscore}\isadigit{0}{\isacharcolon}\ \ \ \ \ \ {\isachardoublequote}rec{\isacharparenleft}\isadigit{0}{\isacharcomma}\ a{\isacharcomma}\ f{\isacharparenright}\ {\isacharequal}\ a{\isachardoublequote}\isanewline
+\ \ rec{\isacharunderscore}Suc{\isacharcolon}\ \ \ \ {\isachardoublequote}rec{\isacharparenleft}Suc{\isacharparenleft}m{\isacharparenright}{\isacharcomma}\ a{\isacharcomma}\ f{\isacharparenright}\ {\isacharequal}\ f{\isacharparenleft}m{\isacharcomma}\ rec{\isacharparenleft}m{\isacharcomma}\ a{\isacharcomma}\ f{\isacharparenright}{\isacharparenright}{\isachardoublequote}\isanewline
\isanewline
\isacommand{constdefs}\isanewline
-\ \ add\ ::\ {\isachardoublequote}{\isacharprime}a::nat\ {\isasymRightarrow}\ {\isacharprime}a\ {\isasymRightarrow}\ {\isacharprime}a{\isachardoublequote}\ \ \ \ {\isacharparenleft}\isakeyword{infixl}\ {\isachardoublequote}+{\isachardoublequote}\ 60{\isacharparenright}\isanewline
-\ \ {\isachardoublequote}m\ +\ n\ {\isasymequiv}\ rec{\isacharparenleft}m,\ n,\ {\isasymlambda}x\ y.\ Suc{\isacharparenleft}y{\isacharparenright}{\isacharparenright}{\isachardoublequote}%
+\ \ add\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequote}{\isacharprime}a{\isacharcolon}{\isacharcolon}nat\ {\isasymRightarrow}\ {\isacharprime}a\ {\isasymRightarrow}\ {\isacharprime}a{\isachardoublequote}\ \ \ \ {\isacharparenleft}\isakeyword{infixl}\ {\isachardoublequote}{\isacharplus}{\isachardoublequote}\ \isadigit{6}\isadigit{0}{\isacharparenright}\isanewline
+\ \ {\isachardoublequote}m\ {\isacharplus}\ n\ {\isasymequiv}\ rec{\isacharparenleft}m{\isacharcomma}\ n{\isacharcomma}\ {\isasymlambda}x\ y{\isachardot}\ Suc{\isacharparenleft}y{\isacharparenright}{\isacharparenright}{\isachardoublequote}%
\begin{isamarkuptext}%
This is an abstract version of the plain $Nat$ theory in
FOL.\footnote{See
--- a/doc-src/AxClass/generated/Product.tex Mon Aug 21 18:49:38 2000 +0200
+++ b/doc-src/AxClass/generated/Product.tex Mon Aug 21 19:03:58 2000 +0200
@@ -1,7 +1,7 @@
\begin{isabelle}%
%
\isamarkupheader{Syntactic classes}
-\isacommand{theory}\ Product\ =\ Main:%
+\isacommand{theory}\ Product\ {\isacharequal}\ Main{\isacharcolon}%
\begin{isamarkuptext}%
\medskip\noindent There is still a feature of Isabelle's type system
left that we have not yet discussed. When declaring polymorphic
@@ -19,7 +19,7 @@
\isacommand{axclass}\isanewline
\ \ product\ {\isacharless}\ {\isachardoublequote}term{\isachardoublequote}\isanewline
\isacommand{consts}\isanewline
-\ \ product\ ::\ {\isachardoublequote}{\isacharprime}a::product\ {\isasymRightarrow}\ {\isacharprime}a\ {\isasymRightarrow}\ {\isacharprime}a{\isachardoublequote}\ \ \ \ {\isacharparenleft}\isakeyword{infixl}\ {\isachardoublequote}{\isasymOtimes}{\isachardoublequote}\ 70{\isacharparenright}%
+\ \ product\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequote}{\isacharprime}a{\isacharcolon}{\isacharcolon}product\ {\isasymRightarrow}\ {\isacharprime}a\ {\isasymRightarrow}\ {\isacharprime}a{\isachardoublequote}\ \ \ \ {\isacharparenleft}\isakeyword{infixl}\ {\isachardoublequote}{\isasymOtimes}{\isachardoublequote}\ \isadigit{7}\isadigit{0}{\isacharparenright}%
\begin{isamarkuptext}%
Here class $product$ is defined as subclass of $term$ without any
additional axioms. This effects in logical equivalence of $product$
@@ -48,10 +48,10 @@
This is done for class $product$ and type $bool$ as follows.%
\end{isamarkuptext}%
-\isacommand{instance}\ bool\ ::\ product\isanewline
+\isacommand{instance}\ bool\ {\isacharcolon}{\isacharcolon}\ product\isanewline
\ \ \isacommand{by}\ intro{\isacharunderscore}classes\isanewline
\isacommand{defs}\ {\isacharparenleft}\isakeyword{overloaded}{\isacharparenright}\isanewline
-\ \ product{\isacharunderscore}bool{\isacharunderscore}def:\ {\isachardoublequote}x\ {\isasymOtimes}\ y\ {\isasymequiv}\ x\ {\isasymand}\ y{\isachardoublequote}%
+\ \ product{\isacharunderscore}bool{\isacharunderscore}def{\isacharcolon}\ {\isachardoublequote}x\ {\isasymOtimes}\ y\ {\isasymequiv}\ x\ {\isasymand}\ y{\isachardoublequote}%
\begin{isamarkuptext}%
The definition $prod_bool_def$ becomes syntactically well-formed only
after the arity $bool :: product$ is made known to the type checker.
--- a/doc-src/AxClass/generated/Semigroups.tex Mon Aug 21 18:49:38 2000 +0200
+++ b/doc-src/AxClass/generated/Semigroups.tex Mon Aug 21 19:03:58 2000 +0200
@@ -1,7 +1,7 @@
\begin{isabelle}%
%
\isamarkupheader{Semigroups}
-\isacommand{theory}\ Semigroups\ =\ Main:%
+\isacommand{theory}\ Semigroups\ {\isacharequal}\ Main{\isacharcolon}%
\begin{isamarkuptext}%
\medskip\noindent An axiomatic type class is simply a class of types
that all meet certain properties, which are also called \emph{class
@@ -15,10 +15,10 @@
semigroups.%
\end{isamarkuptext}%
\isacommand{consts}\isanewline
-\ \ times\ ::\ {\isachardoublequote}{\isacharprime}a\ {\isasymRightarrow}\ {\isacharprime}a\ {\isasymRightarrow}\ {\isacharprime}a{\isachardoublequote}\ \ \ \ {\isacharparenleft}\isakeyword{infixl}\ {\isachardoublequote}{\isasymOtimes}{\isachardoublequote}\ 70{\isacharparenright}\isanewline
+\ \ times\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequote}{\isacharprime}a\ {\isasymRightarrow}\ {\isacharprime}a\ {\isasymRightarrow}\ {\isacharprime}a{\isachardoublequote}\ \ \ \ {\isacharparenleft}\isakeyword{infixl}\ {\isachardoublequote}{\isasymOtimes}{\isachardoublequote}\ \isadigit{7}\isadigit{0}{\isacharparenright}\isanewline
\isacommand{axclass}\isanewline
\ \ semigroup\ {\isacharless}\ {\isachardoublequote}term{\isachardoublequote}\isanewline
-\ \ assoc:\ {\isachardoublequote}{\isacharparenleft}x\ {\isasymOtimes}\ y{\isacharparenright}\ {\isasymOtimes}\ z\ =\ x\ {\isasymOtimes}\ {\isacharparenleft}y\ {\isasymOtimes}\ z{\isacharparenright}{\isachardoublequote}%
+\ \ assoc{\isacharcolon}\ {\isachardoublequote}{\isacharparenleft}x\ {\isasymOtimes}\ y{\isacharparenright}\ {\isasymOtimes}\ z\ {\isacharequal}\ x\ {\isasymOtimes}\ {\isacharparenleft}y\ {\isasymOtimes}\ z{\isacharparenright}{\isachardoublequote}%
\begin{isamarkuptext}%
\noindent Above we have first declared a polymorphic constant $\TIMES
:: \alpha \To \alpha \To \alpha$ and then defined the class
@@ -37,10 +37,10 @@
to semigroups $(\tau, \TIMES^\tau)$.%
\end{isamarkuptext}%
\isacommand{consts}\isanewline
-\ \ plus\ ::\ {\isachardoublequote}{\isacharprime}a\ {\isasymRightarrow}\ {\isacharprime}a\ {\isasymRightarrow}\ {\isacharprime}a{\isachardoublequote}\ \ \ \ {\isacharparenleft}\isakeyword{infixl}\ {\isachardoublequote}{\isasymOplus}{\isachardoublequote}\ 70{\isacharparenright}\isanewline
+\ \ plus\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequote}{\isacharprime}a\ {\isasymRightarrow}\ {\isacharprime}a\ {\isasymRightarrow}\ {\isacharprime}a{\isachardoublequote}\ \ \ \ {\isacharparenleft}\isakeyword{infixl}\ {\isachardoublequote}{\isasymOplus}{\isachardoublequote}\ \isadigit{7}\isadigit{0}{\isacharparenright}\isanewline
\isacommand{axclass}\isanewline
\ \ plus{\isacharunderscore}semigroup\ {\isacharless}\ {\isachardoublequote}term{\isachardoublequote}\isanewline
-\ \ assoc:\ {\isachardoublequote}{\isacharparenleft}x\ {\isasymOplus}\ y{\isacharparenright}\ {\isasymOplus}\ z\ =\ x\ {\isasymOplus}\ {\isacharparenleft}y\ {\isasymOplus}\ z{\isacharparenright}{\isachardoublequote}%
+\ \ assoc{\isacharcolon}\ {\isachardoublequote}{\isacharparenleft}x\ {\isasymOplus}\ y{\isacharparenright}\ {\isasymOplus}\ z\ {\isacharequal}\ x\ {\isasymOplus}\ {\isacharparenleft}y\ {\isasymOplus}\ z{\isacharparenright}{\isachardoublequote}%
\begin{isamarkuptext}%
\noindent Even if classes $plus_semigroup$ and $semigroup$ both
represent semigroups in a sense, they are certainly not quite the
--- a/doc-src/AxClass/generated/isabelle.sty Mon Aug 21 18:49:38 2000 +0200
+++ b/doc-src/AxClass/generated/isabelle.sty Mon Aug 21 19:03:58 2000 +0200
@@ -9,6 +9,7 @@
% isabelle environments
\newcommand{\isastyle}{\small\tt\slshape}
+\newcommand{\isastyleminor}{\small\tt\slshape}
\newcommand{\isastyletext}{\normalsize\rm}
\newcommand{\isastyletxt}{\rm}
\newcommand{\isastylecmt}{\rm}
@@ -20,10 +21,13 @@
\isa@parskip\parskip\parskip0pt%
\isastyle}{}
-\newcommand{\isa}[1]{\emph{\isastyle #1}}
+\newcommand{\isa}[1]{\emph{\isastyleminor #1}}
\newcommand{\isanewline}{\mbox{}\\\mbox{}}
+\newcommand{\isadigit}[1]{#1}
+\chardef\isacharbang=`\!
+\chardef\isachardoublequote=`\"
\chardef\isacharhash=`\#
\chardef\isachardollar=`\$
\chardef\isacharpercent=`\%
@@ -32,15 +36,24 @@
\chardef\isacharparenleft=`\(
\chardef\isacharparenright=`\)
\chardef\isacharasterisk=`\*
+\chardef\isacharplus=`\+
+\chardef\isacharcomma=`\,
\chardef\isacharminus=`\-
+\chardef\isachardot=`\.
+\chardef\isacharslash=`\/
+\chardef\isacharcolon=`\:
+\chardef\isacharsemicolon=`\;
\chardef\isacharless=`\<
+\chardef\isacharequal=`\=
\chardef\isachargreater=`\>
+\chardef\isacharquery=`\?
+\chardef\isacharat=`\@
\chardef\isacharbrackleft=`\[
-\chardef\isachardoublequote=`\"
\chardef\isacharbackslash=`\\
\chardef\isacharbrackright=`\]
\chardef\isacharcircum=`\^
\chardef\isacharunderscore=`\_
+\chardef\isacharbackquote=`\`
\chardef\isacharbraceleft=`\{
\chardef\isacharbar=`\|
\chardef\isacharbraceright=`\}
@@ -49,10 +62,10 @@
% keyword and section markup
-\newcommand{\isacommand}[1]{\emph{\bf #1}}
-\newcommand{\isakeyword}[1]{\emph{\bf #1}}
-\newcommand{\isabeginblock}{\isakeyword{\{}}
-\newcommand{\isaendblock}{\isakeyword{\}}}
+\newcommand{\isakeyword}[1]
+{\emph{\bf\def\isachardot{.}\def\isacharunderscore{-}%
+\def\isacharbraceleft{\{}\def\isacharbraceright{\}}#1}}
+\newcommand{\isacommand}[1]{\isakeyword{#1}}
\newcommand{\isamarkupheader}[1]{\section{#1}}
\newcommand{\isamarkupchapter}[1]{\chapter{#1}}
@@ -72,23 +85,34 @@
% alternative styles -- default is "tt"
\newcommand{\isabellestyle}{}
-\def\isabellestyle#1{\csname isasetup#1\endcsname}
+\def\isabellestyle#1{\csname isabellestyle#1\endcsname}
-\newcommand{\isasetupit}{%
-\renewcommand{\isastyle}{\small\itshape}%
-\renewcommand{\isastyletext}{\normalsize\rm}%
-\renewcommand{\isastyletxt}{\rm}%
-\renewcommand{\isastylecmt}{\rm}%
-\renewcommand{\isachardollar}{\textsl{\$}}%
-\renewcommand{\isacharampersand}{\textsl{\&}}%
-\renewcommand{\isacharprime}{$'$}%
+\newcommand{\isabellestyleit}{%
+\renewcommand{\isastyle}{\small\it}%
+\renewcommand{\isastyleminor}{\it}%
+%\renewcommand{\isadigit}[1]{\emph{$##1$}}
+\renewcommand{\isacharbang}{\emph{$!$}}%
+\renewcommand{\isachardoublequote}{}%
+\renewcommand{\isacharhash}{\emph{$\#$}}%
+\renewcommand{\isachardollar}{\emph{$\$$}}%
+\renewcommand{\isacharpercent}{\emph{$\%$}}%
+\renewcommand{\isacharampersand}{\emph{$\&$}}%
+\renewcommand{\isacharprime}{$\mskip2mu{'}\mskip-2mu$}%
\renewcommand{\isacharparenleft}{\emph{$($}}%
\renewcommand{\isacharparenright}{\emph{$)$}}%
\renewcommand{\isacharasterisk}{\emph{$*$}}%
+\renewcommand{\isacharplus}{\emph{$+$}}%
+\renewcommand{\isacharcomma}{\emph{$\mathord,$}}%
\renewcommand{\isacharminus}{\emph{$-$}}%
+\renewcommand{\isachardot}{\emph{$\mathord.$}}%
+\renewcommand{\isacharslash}{\emph{$/$}}%
+\renewcommand{\isacharcolon}{\emph{$\mathord:$}}%
+\renewcommand{\isacharsemicolon}{\emph{$\mathord;$}}%
\renewcommand{\isacharless}{\emph{$<$}}%
+\renewcommand{\isacharequal}{\emph{$=$}}%
\renewcommand{\isachargreater}{\emph{$>$}}%
-\renewcommand{\isachardoublequote}{}%
+%\renewcommand{\isacharquery}{\emph{$\mathord?$}}%
+\renewcommand{\isacharat}{\emph{$@$}}%
\renewcommand{\isacharbrackleft}{\emph{$[$}}%
\renewcommand{\isacharbrackright}{\emph{$]$}}%
\renewcommand{\isacharunderscore}{-}%
@@ -97,5 +121,4 @@
\renewcommand{\isacharbraceright}{\emph{$\}$}}%
}
-\newcommand{\isasetupsl}{\isasetupit\renewcommand{\isastyle}{\small\slshape}}
-
+\newcommand{\isabellestylesl}{\isabellestyleit\renewcommand{\isastyle}{\small\slshape}}