--- a/src/HOL/Library/Quotient.thy Sun Oct 22 22:18:40 2000 +0200
+++ b/src/HOL/Library/Quotient.thy Sun Oct 22 22:23:16 2000 +0200
@@ -70,8 +70,8 @@
subsection {* Equality on quotients *}
text {*
- Equality of canonical quotient elements corresponds to the original
- relation as follows.
+ Equality of canonical quotient elements coincides with the original
+ relation.
*}
theorem equivalence_class_eq [iff?]: "(\<lfloor>a\<rfloor> = \<lfloor>b\<rfloor>) = (a \<sim> b)"
--- a/src/HOL/Library/document/root.tex Sun Oct 22 22:18:40 2000 +0200
+++ b/src/HOL/Library/document/root.tex Sun Oct 22 22:23:16 2000 +0200
@@ -26,9 +26,9 @@
\newcommand{\isabelletitle}{}\newcommand{\title}[1]{\gdef\isabelletitle{#1}}
\newcommand{\isabelleauthor}{}\newcommand{\author}[1]{\gdef\isabelleauthor{#1}}
\renewcommand{\isamarkupheader}[1]%
-{\newpage\title{***~Theory ``\isabellecontext'': unknown title}\author{}#1%
+{\title{***~Theory ``\isabellecontext'': unknown title}\author{}#1%
+\ifthenelse{\equal{}{\isabelletitle}}{}{\newpage\section{\isabelletitle}}%
\markright{THEORY~``\isabellecontext''}
-\ifthenelse{\equal{}{\isabelletitle}}{}{\section{\isabelletitle}}%
\ifthenelse{\equal{}{\isabelleauthor}}{}%
{{\flushright\footnotesize\sl (By \isabelleauthor)\par\bigskip}}}