# HG changeset patch
# User wenzelm
# Date 958984304 -7200
# Node ID fc7841f313880ea1bf6ba1359a2cae284fb37813
# Parent  4f0f79fe41b9da150f7308f75e17c60fb3979d93
tuned;

diff -r 4f0f79fe41b9 -r fc7841f31388 doc-src/AxClass/Group/ROOT.ML
--- a/doc-src/AxClass/Group/ROOT.ML	Mon May 22 10:02:58 2000 +0200
+++ b/doc-src/AxClass/Group/ROOT.ML	Mon May 22 10:31:44 2000 +0200
@@ -1,5 +1,4 @@
 
-use_thy "Semigroup";
 use_thy "Semigroups";
 use_thy "Group";
 use_thy "Product";
diff -r 4f0f79fe41b9 -r fc7841f31388 doc-src/AxClass/Group/Semigroup.thy
--- a/doc-src/AxClass/Group/Semigroup.thy	Mon May 22 10:02:58 2000 +0200
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,9 +0,0 @@
-theory Semigroup = Main:;
-
-consts
-  times :: "'a \\<Rightarrow> 'a \\<Rightarrow> 'a"    (infixl "\<Otimes>" 70);
-axclass
-  semigroup < "term"
-  assoc: "(x \<Otimes> y) \<Otimes> z = x \<Otimes> (y \<Otimes> z)";
-
-end;
\ No newline at end of file
diff -r 4f0f79fe41b9 -r fc7841f31388 doc-src/AxClass/Group/Semigroups.thy
--- a/doc-src/AxClass/Group/Semigroups.thy	Mon May 22 10:02:58 2000 +0200
+++ b/doc-src/AxClass/Group/Semigroups.thy	Mon May 22 10:31:44 2000 +0200
@@ -1,19 +1,54 @@
+
+header {* Semigroups *};
+
 theory Semigroups = Main:;
 
-constdefs
-  is_assoc :: "('a \\<Rightarrow> 'a \\<Rightarrow> 'a) \\<Rightarrow> bool"
-  "is_assoc f \\<equiv> \\<forall>x y z. f (f x y) z = f x (f y z)";
+text {*
+ \medskip\noindent An axiomatic type class is simply a class of types
+ that all meet certain \emph{axioms}. Thus, type classes may be also
+ understood as type predicates --- i.e.\ abstractions over a single
+ type argument $\alpha$.  Class axioms typically contain polymorphic
+ constants that depend on this type $\alpha$.  These
+ \emph{characteristic constants} behave like operations associated
+ with the ``carrier'' type $\alpha$.
+
+ We illustrate these basic concepts by the following formulation of
+ semigroups.
+*};
 
 consts
-  plus :: "'a \\<Rightarrow> 'a \\<Rightarrow> 'a"    (infixl "\<Oplus>" 65);
+  times :: "'a \\<Rightarrow> 'a \\<Rightarrow> 'a"    (infixl "\<Otimes>" 70);
+axclass
+  semigroup < "term"
+  assoc: "(x \<Otimes> y) \<Otimes> z = x \<Otimes> (y \<Otimes> z)";
+
+text {*
+ \noindent Above we have first declared a polymorphic constant $\TIMES
+ :: \alpha \To \alpha \To \alpha$ and then defined the class
+ $semigroup$ of all types $\tau$ such that $\TIMES :: \tau \To \tau
+ \To \tau$ is indeed an associative operator.  The $assoc$ axiom
+ contains exactly one type variable, which is invisible in the above
+ presentation, though.  Also note that free term variables (like $x$,
+ $y$, $z$) are allowed for user convenience --- conceptually all of
+ these are bound by outermost universal quantifiers.
+
+ \medskip In general, type classes may be used to describe
+ \emph{structures} with exactly one carrier $\alpha$ and a fixed
+ \emph{signature}.  Different signatures require different classes.
+ Subsequently, class $plus_semigroup$ represents semigroups of the
+ form $(\tau, \PLUS^\tau)$, while $semigroup$ above would correspond
+ to semigroups $(\tau, \TIMES^\tau)$.
+*};
+
+consts
+  plus :: "'a \\<Rightarrow> 'a \\<Rightarrow> 'a"    (infixl "\<Oplus>" 70);
 axclass
   plus_semigroup < "term"
-  assoc: "is_assoc (op \<Oplus>)";
+  assoc: "(x \<Oplus> y) \<Oplus> z = x \<Oplus> (y \<Oplus> z)";
 
-consts
-  times :: "'a \\<Rightarrow> 'a \\<Rightarrow> 'a"    (infixl "\<Otimes>" 65);
-axclass
-  times_semigroup < "term"
-  assoc: "is_assoc (op \<Otimes>)";
+text {*
+ \noindent Even if classes $plus_semigroup$ and $times_semigroup$ both
+ represent semigroups in a sense, they are certainly not the same!
+*};
 
 end;
\ No newline at end of file
diff -r 4f0f79fe41b9 -r fc7841f31388 doc-src/AxClass/IsaMakefile
--- a/doc-src/AxClass/IsaMakefile	Mon May 22 10:02:58 2000 +0200
+++ b/doc-src/AxClass/IsaMakefile	Mon May 22 10:31:44 2000 +0200
@@ -24,8 +24,9 @@
 	@cd $(SRC)/HOL; $(ISATOOL) make HOL
 
 $(LOG)/HOL-Group.gz: $(OUT)/HOL Group/ROOT.ML Group/document/root.tex \
-  Group/Group.thy Group/Product.thy Group/Semigroup.thy Group/Semigroups.thy
+  Group/Group.thy Group/Product.thy Group/Semigroups.thy
 	@$(USEDIR) $(OUT)/HOL Group
+	@rm -f generated/pdfsetup.sty generated/session.tex
 
 
 ## Nat
@@ -38,6 +39,7 @@
 $(LOG)/FOL-Nat.gz: $(OUT)/FOL Nat/ROOT.ML Nat/document/root.tex \
   Nat/NatClass.ML Nat/NatClass.thy
 	@$(USEDIR) $(OUT)/FOL Nat
+	@rm -f generated/pdfsetup.sty generated/session.tex
 
 
 ## clean
diff -r 4f0f79fe41b9 -r fc7841f31388 doc-src/AxClass/Makefile
--- a/doc-src/AxClass/Makefile	Mon May 22 10:02:58 2000 +0200
+++ b/doc-src/AxClass/Makefile	Mon May 22 10:31:44 2000 +0200
@@ -15,8 +15,7 @@
 
 FILES = axclass.tex body.tex ../iman.sty ../extra.sty ../isar.sty \
   ../pdfsetup.sty generated/Group.tex generated/NatClass.tex \
-  generated/Product.tex generated/Semigroup.tex generated/Semigroups.tex \
-  generated/session.tex
+  generated/Product.tex generated/Semigroups.tex
 
 dvi: $(NAME).dvi
 
diff -r 4f0f79fe41b9 -r fc7841f31388 doc-src/AxClass/Nat/NatClass.thy
--- a/doc-src/AxClass/Nat/NatClass.thy	Mon May 22 10:02:58 2000 +0200
+++ b/doc-src/AxClass/Nat/NatClass.thy	Mon May 22 10:31:44 2000 +0200
@@ -1,5 +1,19 @@
+
+header {* Defining natural numbers in FOL \label{sec:ex-natclass} *};
+
 theory NatClass = FOL:;
 
+text {*
+ \medskip\noindent Axiomatic type classes abstract over exactly one
+ type argument. Thus, any \emph{axiomatic} theory extension where each
+ axiom refers to at most one type variable, may be trivially turned
+ into a \emph{definitional} one.
+
+ We illustrate this with the natural numbers in
+ Isabelle/FOL.\footnote{See also
+ \url{http://isabelle.in.tum.de/library/FOL/ex/NatClass.html}}
+*};
+
 consts
   zero :: 'a    ("0")
   Suc :: "'a \\<Rightarrow> 'a"
@@ -17,4 +31,30 @@
   add :: "'a::nat \\<Rightarrow> 'a \\<Rightarrow> 'a"    (infixl "+" 60)
   "m + n \\<equiv> rec(m, n, \\<lambda>x y. Suc(y))";
 
+text {*
+ This is an abstract version of the plain $Nat$ theory in
+ FOL.\footnote{See
+ \url{http://isabelle.in.tum.de/library/FOL/ex/Nat.html}}
+
+ Basically, we have just replaced all occurrences of type $nat$ by
+ $\alpha$ and used the natural number axioms to define class $nat$.
+ There is only a minor snag, that the original recursion operator
+ $rec$ had to be made monomorphic, in a sense.  Thus class $nat$
+ contains exactly those types $\tau$ that are isomorphic to ``the''
+ natural numbers (with signature $0$, $Suc$, $rec$).
+
+ \medskip What we have done here can be also viewed as \emph{type
+ specification}.  Of course, it still remains open if there is some
+ type at all that meets the class axioms.  Now a very nice property of
+ axiomatic type classes is, that abstract reasoning is always possible
+ --- independent of satisfiability.  The meta-logic won't break, even
+ if some classes (or general sorts) turns out to be empty
+ (``inconsistent'') later.
+
+ Theorems of the abstract natural numbers may be derived in the same
+ way as for the concrete version.  The original proof scripts may be
+ used with some trivial changes only (mostly adding some type
+ constraints).
+*};
+
 end;
\ No newline at end of file
diff -r 4f0f79fe41b9 -r fc7841f31388 doc-src/AxClass/body.tex
--- a/doc-src/AxClass/body.tex	Mon May 22 10:02:58 2000 +0200
+++ b/doc-src/AxClass/body.tex	Mon May 22 10:31:44 2000 +0200
@@ -46,84 +46,13 @@
 formulated within HOL, except the one of \secref{sec:ex-natclass} which is in
 FOL.
 
-\section{Semigroups}
-
-An axiomatic type class is simply a class of types that all meet certain
-\emph{axioms}. Thus, type classes may be also understood as type predicates
---- i.e.\ abstractions over a single type argument $\alpha$.  Class axioms
-typically contain polymorphic constants that depend on this type $\alpha$.
-These \emph{characteristic constants} behave like operations associated with
-the ``carrier'' type $\alpha$.
-
-We illustrate these basic concepts by the following theory of semigroups.
-
-\bigskip
-\input{generated/Semigroup}
-\bigskip
-
-\noindent
-Above we have first declared a polymorphic constant $\TIMES :: \alpha \To
-\alpha \To \alpha$ and then defined the class $semigroup$ of all types $\tau$
-such that $\TIMES :: \tau \To \tau \To \tau$ is indeed an associative
-operator.  The $assoc$ axiom contains exactly one type variable, which is
-invisible in the above presentation, though.  Also note that free term
-variables (like $x$, $y$, $z$) are allowed for user convenience ---
-conceptually all of these are bound by outermost universal quantifiers.
-
-\medskip
-
-In general, type classes may be used to describe \emph{structures} with
-exactly one carrier $\alpha$ and a fixed \emph{signature}.  Different
-signatures require different classes. In the following theory, class
-$plus_semigroup$ represents semigroups of the form $(\tau, \PLUS^\tau)$ while
-$times_semigroup$ represents semigroups $(\tau, \TIMES^\tau)$.
-
-\bigskip
 \input{generated/Semigroups}
-\bigskip
-
-\noindent Even if classes $plus_semigroup$ and $times_semigroup$ both represent
-semigroups in a sense, they are not the same!
-
 
 \input{generated/Group}
 
 \input{generated/Product}
 
-
-\section{Defining natural numbers in FOL}\label{sec:ex-natclass}
-
-Axiomatic type classes abstract over exactly one type argument. Thus, any
-\emph{axiomatic} theory extension where each axiom refers to at most one type
-variable, may be trivially turned into a \emph{definitional} one.
-
-We illustrate this with the natural numbers in Isabelle/FOL.
-
-\bigskip
 \input{generated/NatClass}
-\bigskip
-
-This is an abstract version of the plain $Nat$ theory in
-FOL.\footnote{See \url{http://isabelle.in.tum.de/library/FOL/ex/Nat.html}}
-
-Basically, we have just replaced all occurrences of type $nat$ by $\alpha$ and
-used the natural number axioms to define class $nat$.  There is only a minor
-snag, that the original recursion operator $rec$ had to be made monomorphic,
-in a sense.  Thus class $nat$ contains exactly those types $\tau$ that are
-isomorphic to ``the'' natural numbers (with signature $0$, $Suc$, $rec$).
-
-\medskip
-
-What we have done here can be also viewed as \emph{type specification}.  Of
-course, it still remains open if there is some type at all that meets the
-class axioms.  Now a very nice property of axiomatic type classes is, that
-abstract reasoning is always possible --- independent of satisfiability.  The
-meta-logic won't break, even if some classes (or general sorts) turns out to
-be empty (``inconsistent'') later.
-
-Theorems of the abstract natural numbers may be derived in the same way as for
-the concrete version.  The original proof scripts may be used with some
-trivial changes only (mostly adding some type constraints).
 
 
 %% FIXME move some parts to ref or isar-ref manual (!?);
@@ -151,7 +80,7 @@
 % \emphnd{matharray}
 
 % Where $c, c@1, \ldots, c@n$ are classes (category $id$ or
-% $string$) and $axm@1, \ldots, axm@m$ (with $m \ge
+% $string$) and $axm@1, \ldots, axm@m$ (with $m \geq
 % 0$) are formulas (category $string$).
 
 % Class $c$ has to be new, and sort $\{c@1, \ldots, c@n\}$ a subsort of
diff -r 4f0f79fe41b9 -r fc7841f31388 doc-src/AxClass/generated/NatClass.tex
--- a/doc-src/AxClass/generated/NatClass.tex	Mon May 22 10:02:58 2000 +0200
+++ b/doc-src/AxClass/generated/NatClass.tex	Mon May 22 10:31:44 2000 +0200
@@ -1,6 +1,17 @@
 \begin{isabelle}%
-\isacommand{theory}~NatClass~=~FOL:\isanewline
-\isanewline
+%
+\isamarkupheader{Defining natural numbers in FOL \label{sec:ex-natclass}}
+\isacommand{theory}~NatClass~=~FOL:%
+\begin{isamarkuptext}%
+\medskip\noindent Axiomatic type classes abstract over exactly one
+ type argument. Thus, any \emph{axiomatic} theory extension where each
+ axiom refers to at most one type variable, may be trivially turned
+ into a \emph{definitional} one.
+
+ We illustrate this with the natural numbers in
+ Isabelle/FOL.\footnote{See also
+ \url{http://isabelle.in.tum.de/library/FOL/ex/NatClass.html}}%
+\end{isamarkuptext}%
 \isacommand{consts}\isanewline
 ~~zero~::~'a~~~~({"}0{"})\isanewline
 ~~Suc~::~{"}'a~{\isasymRightarrow}~'a{"}\isanewline
@@ -16,6 +27,30 @@
 \isanewline
 \isacommand{constdefs}\isanewline
 ~~add~::~{"}'a::nat~{\isasymRightarrow}~'a~{\isasymRightarrow}~'a{"}~~~~(\isakeyword{infixl}~{"}+{"}~60)\isanewline
-~~{"}m~+~n~{\isasymequiv}~rec(m,~n,~{\isasymlambda}x~y.~Suc(y)){"}\isanewline
-\isanewline
+~~{"}m~+~n~{\isasymequiv}~rec(m,~n,~{\isasymlambda}x~y.~Suc(y)){"}%
+\begin{isamarkuptext}%
+This is an abstract version of the plain $Nat$ theory in
+ FOL.\footnote{See
+ \url{http://isabelle.in.tum.de/library/FOL/ex/Nat.html}}
+
+ Basically, we have just replaced all occurrences of type $nat$ by
+ $\alpha$ and used the natural number axioms to define class $nat$.
+ There is only a minor snag, that the original recursion operator
+ $rec$ had to be made monomorphic, in a sense.  Thus class $nat$
+ contains exactly those types $\tau$ that are isomorphic to ``the''
+ natural numbers (with signature $0$, $Suc$, $rec$).
+
+ \medskip What we have done here can be also viewed as \emph{type
+ specification}.  Of course, it still remains open if there is some
+ type at all that meets the class axioms.  Now a very nice property of
+ axiomatic type classes is, that abstract reasoning is always possible
+ --- independent of satisfiability.  The meta-logic won't break, even
+ if some classes (or general sorts) turns out to be empty
+ (``inconsistent'') later.
+
+ Theorems of the abstract natural numbers may be derived in the same
+ way as for the concrete version.  The original proof scripts may be
+ used with some trivial changes only (mostly adding some type
+ constraints).%
+\end{isamarkuptext}%
 \isacommand{end}\end{isabelle}%
diff -r 4f0f79fe41b9 -r fc7841f31388 doc-src/AxClass/generated/Semigroup.tex
--- a/doc-src/AxClass/generated/Semigroup.tex	Mon May 22 10:02:58 2000 +0200
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,10 +0,0 @@
-\begin{isabelle}%
-\isacommand{theory}~Semigroup~=~Main:\isanewline
-\isanewline
-\isacommand{consts}\isanewline
-~~times~::~{"}'a~{\isasymRightarrow}~'a~{\isasymRightarrow}~'a{"}~~~~(\isakeyword{infixl}~{"}{\isasymOtimes}{"}~70)\isanewline
-\isacommand{axclass}\isanewline
-~~semigroup~<~{"}term{"}\isanewline
-~~assoc:~{"}(x~{\isasymOtimes}~y)~{\isasymOtimes}~z~=~x~{\isasymOtimes}~(y~{\isasymOtimes}~z){"}\isanewline
-\isanewline
-\isacommand{end}\end{isabelle}%
diff -r 4f0f79fe41b9 -r fc7841f31388 doc-src/AxClass/generated/Semigroups.tex
--- a/doc-src/AxClass/generated/Semigroups.tex	Mon May 22 10:02:58 2000 +0200
+++ b/doc-src/AxClass/generated/Semigroups.tex	Mon May 22 10:31:44 2000 +0200
@@ -1,20 +1,48 @@
 \begin{isabelle}%
-\isacommand{theory}~Semigroups~=~Main:\isanewline
-\isanewline
-\isacommand{constdefs}\isanewline
-~~is\_assoc~::~{"}('a~{\isasymRightarrow}~'a~{\isasymRightarrow}~'a)~{\isasymRightarrow}~bool{"}\isanewline
-~~{"}is\_assoc~f~{\isasymequiv}~{\isasymforall}x~y~z.~f~(f~x~y)~z~=~f~x~(f~y~z){"}\isanewline
-\isanewline
+%
+\isamarkupheader{Semigroups}
+\isacommand{theory}~Semigroups~=~Main:%
+\begin{isamarkuptext}%
+\medskip\noindent An axiomatic type class is simply a class of types
+ that all meet certain \emph{axioms}. Thus, type classes may be also
+ understood as type predicates --- i.e.\ abstractions over a single
+ type argument $\alpha$.  Class axioms typically contain polymorphic
+ constants that depend on this type $\alpha$.  These
+ \emph{characteristic constants} behave like operations associated
+ with the ``carrier'' type $\alpha$.
+
+ We illustrate these basic concepts by the following formulation of
+ semigroups.%
+\end{isamarkuptext}%
 \isacommand{consts}\isanewline
-~~plus~::~{"}'a~{\isasymRightarrow}~'a~{\isasymRightarrow}~'a{"}~~~~(\isakeyword{infixl}~{"}{\isasymOplus}{"}~65)\isanewline
+~~times~::~{"}'a~{\isasymRightarrow}~'a~{\isasymRightarrow}~'a{"}~~~~(\isakeyword{infixl}~{"}{\isasymOtimes}{"}~70)\isanewline
+\isacommand{axclass}\isanewline
+~~semigroup~<~{"}term{"}\isanewline
+~~assoc:~{"}(x~{\isasymOtimes}~y)~{\isasymOtimes}~z~=~x~{\isasymOtimes}~(y~{\isasymOtimes}~z){"}%
+\begin{isamarkuptext}%
+\noindent Above we have first declared a polymorphic constant $\TIMES
+ :: \alpha \To \alpha \To \alpha$ and then defined the class
+ $semigroup$ of all types $\tau$ such that $\TIMES :: \tau \To \tau
+ \To \tau$ is indeed an associative operator.  The $assoc$ axiom
+ contains exactly one type variable, which is invisible in the above
+ presentation, though.  Also note that free term variables (like $x$,
+ $y$, $z$) are allowed for user convenience --- conceptually all of
+ these are bound by outermost universal quantifiers.
+
+ \medskip In general, type classes may be used to describe
+ \emph{structures} with exactly one carrier $\alpha$ and a fixed
+ \emph{signature}.  Different signatures require different classes.
+ Subsequently, class $plus_semigroup$ represents semigroups of the
+ form $(\tau, \PLUS^\tau)$, while $semigroup$ above would correspond
+ to semigroups $(\tau, \TIMES^\tau)$.%
+\end{isamarkuptext}%
+\isacommand{consts}\isanewline
+~~plus~::~{"}'a~{\isasymRightarrow}~'a~{\isasymRightarrow}~'a{"}~~~~(\isakeyword{infixl}~{"}{\isasymOplus}{"}~70)\isanewline
 \isacommand{axclass}\isanewline
 ~~plus\_semigroup~<~{"}term{"}\isanewline
-~~assoc:~{"}is\_assoc~(op~{\isasymOplus}){"}\isanewline
-\isanewline
-\isacommand{consts}\isanewline
-~~times~::~{"}'a~{\isasymRightarrow}~'a~{\isasymRightarrow}~'a{"}~~~~(\isakeyword{infixl}~{"}{\isasymOtimes}{"}~65)\isanewline
-\isacommand{axclass}\isanewline
-~~times\_semigroup~<~{"}term{"}\isanewline
-~~assoc:~{"}is\_assoc~(op~{\isasymOtimes}){"}\isanewline
-\isanewline
+~~assoc:~{"}(x~{\isasymOplus}~y)~{\isasymOplus}~z~=~x~{\isasymOplus}~(y~{\isasymOplus}~z){"}%
+\begin{isamarkuptext}%
+\noindent Even if classes $plus_semigroup$ and $times_semigroup$ both
+ represent semigroups in a sense, they are certainly not the same!%
+\end{isamarkuptext}%
 \isacommand{end}\end{isabelle}%
diff -r 4f0f79fe41b9 -r fc7841f31388 doc-src/AxClass/generated/pdfsetup.sty
--- a/doc-src/AxClass/generated/pdfsetup.sty	Mon May 22 10:02:58 2000 +0200
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,9 +0,0 @@
-%%
-%% $Id$
-%%
-%% conditional url/hyperref setup
-%%
-
-\@ifundefined{pdfoutput}{\usepackage{url}}
-{\usepackage[pdftex,a4paper,colorlinks=true]{hyperref}
-  \IfFileExists{thumbpdf.sty}{\usepackage{thumbpdf}}{}}
diff -r 4f0f79fe41b9 -r fc7841f31388 doc-src/AxClass/generated/session.tex
--- a/doc-src/AxClass/generated/session.tex	Mon May 22 10:02:58 2000 +0200
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,1 +0,0 @@
-\input{NatClass.tex}