tuned;
authorwenzelm
Sun Oct 22 22:23:16 2000 +0200 (2000-10-22)
changeset 10286fdcdb8a80988
parent 10285 6949e17f314a
child 10287 9ab1671398a6
tuned;
src/HOL/Library/Quotient.thy
src/HOL/Library/document/root.tex
     1.1 --- a/src/HOL/Library/Quotient.thy	Sun Oct 22 22:18:40 2000 +0200
     1.2 +++ b/src/HOL/Library/Quotient.thy	Sun Oct 22 22:23:16 2000 +0200
     1.3 @@ -70,8 +70,8 @@
     1.4  subsection {* Equality on quotients *}
     1.5  
     1.6  text {*
     1.7 - Equality of canonical quotient elements corresponds to the original
     1.8 - relation as follows.
     1.9 + Equality of canonical quotient elements coincides with the original
    1.10 + relation.
    1.11  *}
    1.12  
    1.13  theorem equivalence_class_eq [iff?]: "(\<lfloor>a\<rfloor> = \<lfloor>b\<rfloor>) = (a \<sim> b)"
     2.1 --- a/src/HOL/Library/document/root.tex	Sun Oct 22 22:18:40 2000 +0200
     2.2 +++ b/src/HOL/Library/document/root.tex	Sun Oct 22 22:23:16 2000 +0200
     2.3 @@ -26,9 +26,9 @@
     2.4  \newcommand{\isabelletitle}{}\newcommand{\title}[1]{\gdef\isabelletitle{#1}}
     2.5  \newcommand{\isabelleauthor}{}\newcommand{\author}[1]{\gdef\isabelleauthor{#1}}
     2.6  \renewcommand{\isamarkupheader}[1]%
     2.7 -{\newpage\title{***~Theory ``\isabellecontext'': unknown title}\author{}#1%
     2.8 +{\title{***~Theory ``\isabellecontext'': unknown title}\author{}#1%
     2.9 +\ifthenelse{\equal{}{\isabelletitle}}{}{\newpage\section{\isabelletitle}}%
    2.10  \markright{THEORY~``\isabellecontext''}
    2.11 -\ifthenelse{\equal{}{\isabelletitle}}{}{\section{\isabelletitle}}%
    2.12  \ifthenelse{\equal{}{\isabelleauthor}}{}%
    2.13  {{\flushright\footnotesize\sl (By \isabelleauthor)\par\bigskip}}}
    2.14