src/HOL/Real_Asymp/Manual/document/style.sty
author eberlm <eberlm@in.tum.de>
Sun, 22 Jul 2018 19:29:51 +0200
changeset 68677 99b1cf1e2d48
permissions -rw-r--r--
Moved Real_Asymp manual
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
68677
99b1cf1e2d48 Moved Real_Asymp manual
eberlm <eberlm@in.tum.de>
parents:
diff changeset
     1
99b1cf1e2d48 Moved Real_Asymp manual
eberlm <eberlm@in.tum.de>
parents:
diff changeset
     2
%% toc
99b1cf1e2d48 Moved Real_Asymp manual
eberlm <eberlm@in.tum.de>
parents:
diff changeset
     3
\newcommand{\tocentry}[1]{\cleardoublepage\phantomsection\addcontentsline{toc}{chapter}{#1}
99b1cf1e2d48 Moved Real_Asymp manual
eberlm <eberlm@in.tum.de>
parents:
diff changeset
     4
\@mkboth{\MakeUppercase{#1}}{\MakeUppercase{#1}}}
99b1cf1e2d48 Moved Real_Asymp manual
eberlm <eberlm@in.tum.de>
parents:
diff changeset
     5
99b1cf1e2d48 Moved Real_Asymp manual
eberlm <eberlm@in.tum.de>
parents:
diff changeset
     6
%% paragraphs
99b1cf1e2d48 Moved Real_Asymp manual
eberlm <eberlm@in.tum.de>
parents:
diff changeset
     7
\setlength{\parindent}{1em}
99b1cf1e2d48 Moved Real_Asymp manual
eberlm <eberlm@in.tum.de>
parents:
diff changeset
     8
99b1cf1e2d48 Moved Real_Asymp manual
eberlm <eberlm@in.tum.de>
parents:
diff changeset
     9
%% references
99b1cf1e2d48 Moved Real_Asymp manual
eberlm <eberlm@in.tum.de>
parents:
diff changeset
    10
\newcommand{\secref}[1]{\S\ref{#1}}
99b1cf1e2d48 Moved Real_Asymp manual
eberlm <eberlm@in.tum.de>
parents:
diff changeset
    11
\newcommand{\figref}[1]{figure~\ref{#1}}
99b1cf1e2d48 Moved Real_Asymp manual
eberlm <eberlm@in.tum.de>
parents:
diff changeset
    12
99b1cf1e2d48 Moved Real_Asymp manual
eberlm <eberlm@in.tum.de>
parents:
diff changeset
    13
%% logical markup
99b1cf1e2d48 Moved Real_Asymp manual
eberlm <eberlm@in.tum.de>
parents:
diff changeset
    14
\newcommand{\strong}[1]{{\bfseries {#1}}}
99b1cf1e2d48 Moved Real_Asymp manual
eberlm <eberlm@in.tum.de>
parents:
diff changeset
    15
\newcommand{\qn}[1]{\emph{#1}}
99b1cf1e2d48 Moved Real_Asymp manual
eberlm <eberlm@in.tum.de>
parents:
diff changeset
    16
99b1cf1e2d48 Moved Real_Asymp manual
eberlm <eberlm@in.tum.de>
parents:
diff changeset
    17
%% typographic conventions
99b1cf1e2d48 Moved Real_Asymp manual
eberlm <eberlm@in.tum.de>
parents:
diff changeset
    18
\newcommand{\qt}[1]{``{#1}''}
99b1cf1e2d48 Moved Real_Asymp manual
eberlm <eberlm@in.tum.de>
parents:
diff changeset
    19
\newcommand{\ditem}[1]{\item[\isastyletext #1]}
99b1cf1e2d48 Moved Real_Asymp manual
eberlm <eberlm@in.tum.de>
parents:
diff changeset
    20
99b1cf1e2d48 Moved Real_Asymp manual
eberlm <eberlm@in.tum.de>
parents:
diff changeset
    21
%% quote environment
99b1cf1e2d48 Moved Real_Asymp manual
eberlm <eberlm@in.tum.de>
parents:
diff changeset
    22
\isakeeptag{quote}
99b1cf1e2d48 Moved Real_Asymp manual
eberlm <eberlm@in.tum.de>
parents:
diff changeset
    23
\renewenvironment{quote}
99b1cf1e2d48 Moved Real_Asymp manual
eberlm <eberlm@in.tum.de>
parents:
diff changeset
    24
  {\list{}{\leftmargin2em\rightmargin0pt}\parindent0pt\parskip0pt\item\relax}
99b1cf1e2d48 Moved Real_Asymp manual
eberlm <eberlm@in.tum.de>
parents:
diff changeset
    25
  {\endlist}
99b1cf1e2d48 Moved Real_Asymp manual
eberlm <eberlm@in.tum.de>
parents:
diff changeset
    26
\renewcommand{\isatagquote}{\begin{quote}}
99b1cf1e2d48 Moved Real_Asymp manual
eberlm <eberlm@in.tum.de>
parents:
diff changeset
    27
\renewcommand{\endisatagquote}{\end{quote}}
99b1cf1e2d48 Moved Real_Asymp manual
eberlm <eberlm@in.tum.de>
parents:
diff changeset
    28
\newcommand{\quotebreak}{\\[1.2ex]}
99b1cf1e2d48 Moved Real_Asymp manual
eberlm <eberlm@in.tum.de>
parents:
diff changeset
    29
99b1cf1e2d48 Moved Real_Asymp manual
eberlm <eberlm@in.tum.de>
parents:
diff changeset
    30
%% presentation
99b1cf1e2d48 Moved Real_Asymp manual
eberlm <eberlm@in.tum.de>
parents:
diff changeset
    31
\setcounter{secnumdepth}{2} \setcounter{tocdepth}{2}
99b1cf1e2d48 Moved Real_Asymp manual
eberlm <eberlm@in.tum.de>
parents:
diff changeset
    32
99b1cf1e2d48 Moved Real_Asymp manual
eberlm <eberlm@in.tum.de>
parents:
diff changeset
    33
%% character detail
99b1cf1e2d48 Moved Real_Asymp manual
eberlm <eberlm@in.tum.de>
parents:
diff changeset
    34
\renewcommand{\isadigit}[1]{\isamath{#1}}
99b1cf1e2d48 Moved Real_Asymp manual
eberlm <eberlm@in.tum.de>
parents:
diff changeset
    35
\binperiod
99b1cf1e2d48 Moved Real_Asymp manual
eberlm <eberlm@in.tum.de>
parents:
diff changeset
    36
\underscoreoff
99b1cf1e2d48 Moved Real_Asymp manual
eberlm <eberlm@in.tum.de>
parents:
diff changeset
    37
99b1cf1e2d48 Moved Real_Asymp manual
eberlm <eberlm@in.tum.de>
parents:
diff changeset
    38
%% format
99b1cf1e2d48 Moved Real_Asymp manual
eberlm <eberlm@in.tum.de>
parents:
diff changeset
    39
\pagestyle{headings}
99b1cf1e2d48 Moved Real_Asymp manual
eberlm <eberlm@in.tum.de>
parents:
diff changeset
    40
\isabellestyle{it}
99b1cf1e2d48 Moved Real_Asymp manual
eberlm <eberlm@in.tum.de>
parents:
diff changeset
    41
99b1cf1e2d48 Moved Real_Asymp manual
eberlm <eberlm@in.tum.de>
parents:
diff changeset
    42
99b1cf1e2d48 Moved Real_Asymp manual
eberlm <eberlm@in.tum.de>
parents:
diff changeset
    43
%%% Local Variables: 
99b1cf1e2d48 Moved Real_Asymp manual
eberlm <eberlm@in.tum.de>
parents:
diff changeset
    44
%%% mode: latex
99b1cf1e2d48 Moved Real_Asymp manual
eberlm <eberlm@in.tum.de>
parents:
diff changeset
    45
%%% TeX-master: "implementation"
99b1cf1e2d48 Moved Real_Asymp manual
eberlm <eberlm@in.tum.de>
parents:
diff changeset
    46
%%% End: