# HG changeset patch
# User wenzelm
# Date 972246196 -7200
# Node ID fdcdb8a80988c17342f0f5314486b27fdb76f551
# Parent  6949e17f314aea35cd1be67351763d3fd1b54ee1
tuned;

diff -r 6949e17f314a -r fdcdb8a80988 src/HOL/Library/Quotient.thy
--- 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)"
diff -r 6949e17f314a -r fdcdb8a80988 src/HOL/Library/document/root.tex
--- 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}}}