# HG changeset patch # User wenzelm # Date 976819063 -3600 # Node ID 2cc6415c18018fe97f6cb2cb4a218a06d9056dd1 # Parent 337c00fd385b465d9cc75b163c5e9fd787a4b0e6 tuned; diff -r 337c00fd385b -r 2cc6415c1801 src/HOL/Library/document/root.tex --- a/src/HOL/Library/document/root.tex Thu Dec 14 19:37:27 2000 +0100 +++ b/src/HOL/Library/document/root.tex Thu Dec 14 19:37:43 2000 +0100 @@ -26,9 +26,10 @@ \newcommand{\isabelletitle}{}\newcommand{\title}[1]{\gdef\isabelletitle{#1}} \newcommand{\isabelleauthor}{}\newcommand{\author}[1]{\gdef\isabelleauthor{#1}} \renewcommand{\isamarkupheader}[1]% -{\title{***~Theory ``\isabellecontext'': unknown title}\author{}#1% +{\title{***~Theory ``\isabellecontext'': unknown title}\author{}% +#1% \ifthenelse{\equal{}{\isabelletitle}}{}{\newpage\section{\isabelletitle}}% -\markright{THEORY~``\isabellecontext''} +\markright{THEORY~``\isabellecontext''}% \ifthenelse{\equal{}{\isabelleauthor}}{}% {{\flushright\footnotesize\sl (By \isabelleauthor)\par\bigskip}}}