src/Doc/Isar_Ref/document/style.sty
author wenzelm
Sun, 14 Feb 2016 16:30:27 +0100
changeset 62312 5e5a881ebc12
parent 62271 4cfe65cfd369
child 69599 caa7e406056d
permissions -rw-r--r--
command '\<proof>' is an alias for 'sorry', with different typesetting;
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
26738
615e1a86787b basic setup for generated document (cf. ../IsarImplementation);
wenzelm
parents:
diff changeset
     1
%% toc
615e1a86787b basic setup for generated document (cf. ../IsarImplementation);
wenzelm
parents:
diff changeset
     2
\newcommand{\tocentry}[1]{\cleardoublepage\phantomsection\addcontentsline{toc}{chapter}{#1}
615e1a86787b basic setup for generated document (cf. ../IsarImplementation);
wenzelm
parents:
diff changeset
     3
\@mkboth{\MakeUppercase{#1}}{\MakeUppercase{#1}}}
615e1a86787b basic setup for generated document (cf. ../IsarImplementation);
wenzelm
parents:
diff changeset
     4
26865
a3afbb414b69 removed obsolete macros for Isar commands etc.;
wenzelm
parents: 26859
diff changeset
     5
\setcounter{secnumdepth}{2} \setcounter{tocdepth}{2}
a3afbb414b69 removed obsolete macros for Isar commands etc.;
wenzelm
parents: 26859
diff changeset
     6
26738
615e1a86787b basic setup for generated document (cf. ../IsarImplementation);
wenzelm
parents:
diff changeset
     7
%% references
50109
c13dc0b1841c tuned structure of Isabelle/HOL;
wenzelm
parents: 48985
diff changeset
     8
\newcommand{\partref}[1]{part~\ref{#1}}
26738
615e1a86787b basic setup for generated document (cf. ../IsarImplementation);
wenzelm
parents:
diff changeset
     9
\newcommand{\secref}[1]{\S\ref{#1}}
615e1a86787b basic setup for generated document (cf. ../IsarImplementation);
wenzelm
parents:
diff changeset
    10
\newcommand{\chref}[1]{chapter~\ref{#1}}
26759
4f066dfc58d1 more ref macros;
wenzelm
parents: 26738
diff changeset
    11
\newcommand{\Chref}[1]{Chapter~\ref{#1}}
4f066dfc58d1 more ref macros;
wenzelm
parents: 26738
diff changeset
    12
\newcommand{\appref}[1]{appendix~\ref{#1}}
4f066dfc58d1 more ref macros;
wenzelm
parents: 26738
diff changeset
    13
\newcommand{\Appref}[1]{Appendix~\ref{#1}}
26738
615e1a86787b basic setup for generated document (cf. ../IsarImplementation);
wenzelm
parents:
diff changeset
    14
\newcommand{\figref}[1]{figure~\ref{#1}}
26759
4f066dfc58d1 more ref macros;
wenzelm
parents: 26738
diff changeset
    15
\newcommand{\Figref}[1]{Figure~\ref{#1}}
26738
615e1a86787b basic setup for generated document (cf. ../IsarImplementation);
wenzelm
parents:
diff changeset
    16
47586
3b89d59a944b accomodate digits within Isar command names, notably 'try0';
wenzelm
parents: 45646
diff changeset
    17
%% Isar
3b89d59a944b accomodate digits within Isar command names, notably 'try0';
wenzelm
parents: 45646
diff changeset
    18
\newcommand{\isasymBBAR}{{\,\newdimen{\tmpheight}\settoheight\tmpheight{\isacharbar}\rule{1pt}{\tmpheight}\,}}
3b89d59a944b accomodate digits within Isar command names, notably 'try0';
wenzelm
parents: 45646
diff changeset
    19
\renewcommand{\isacommand}[1]{\isakeyword{\isadigitreset#1}}
3b89d59a944b accomodate digits within Isar command names, notably 'try0';
wenzelm
parents: 45646
diff changeset
    20
28760
cbc435f7b16b unified use of declaration environment with IsarImplementation;
wenzelm
parents: 28758
diff changeset
    21
%% ML
28763
b5e6122ff575 added pretty printing options (from old ref manual);
wenzelm
parents: 28760
diff changeset
    22
\newenvironment{mldecls}{\par\noindent\begingroup\def\isanewline{\\}\begin{tabular}{ll}}{\end{tabular}\medskip\endgroup}
28758
4ce896a30f88 added bind_thm, bind_thms;
wenzelm
parents: 26865
diff changeset
    23
47586
3b89d59a944b accomodate digits within Isar command names, notably 'try0';
wenzelm
parents: 45646
diff changeset
    24
\renewcommand{\isatagML}{\begingroup\isabellestyle{default}\isastyle\isadigitreset}
42654
b1a051891ec4 tag ML as in IsarImplementation;
wenzelm
parents: 42631
diff changeset
    25
\renewcommand{\endisatagML}{\endgroup}
b1a051891ec4 tag ML as in IsarImplementation;
wenzelm
parents: 42631
diff changeset
    26
26859
b9ab6246765e removed obsolete macros;
wenzelm
parents: 26778
diff changeset
    27
%% math
29725
03916d2d16d3 some more macros;
wenzelm
parents: 28763
diff changeset
    28
\newcommand{\isasymstrut}{\isamath{\mathstrut}}
03916d2d16d3 some more macros;
wenzelm
parents: 28763
diff changeset
    29
\newcommand{\isasymvartheta}{\isamath{\,\theta}}
26859
b9ab6246765e removed obsolete macros;
wenzelm
parents: 26778
diff changeset
    30
\newcommand{\isactrlvec}[1]{\emph{$\overline{#1}$}}
b9ab6246765e removed obsolete macros;
wenzelm
parents: 26778
diff changeset
    31
\renewcommand{\isadigit}[1]{\isamath{#1}}
26738
615e1a86787b basic setup for generated document (cf. ../IsarImplementation);
wenzelm
parents:
diff changeset
    32
26865
a3afbb414b69 removed obsolete macros for Isar commands etc.;
wenzelm
parents: 26859
diff changeset
    33
%% global style options
26738
615e1a86787b basic setup for generated document (cf. ../IsarImplementation);
wenzelm
parents:
diff changeset
    34
\pagestyle{headings}
615e1a86787b basic setup for generated document (cf. ../IsarImplementation);
wenzelm
parents:
diff changeset
    35
\sloppy
615e1a86787b basic setup for generated document (cf. ../IsarImplementation);
wenzelm
parents:
diff changeset
    36
42656
89132fbd852a sane paragraph layout;
wenzelm
parents: 42654
diff changeset
    37
\parindent 0pt\parskip 0.5ex
89132fbd852a sane paragraph layout;
wenzelm
parents: 42654
diff changeset
    38
55365
9d5aba2baa4c yet another attempt at actual underscore;
wenzelm
parents: 50109
diff changeset
    39
\isabellestyle{literalunderscore}
42631
028f94955436 proper treatment of underscore in rail diagrams;
wenzelm
parents: 30242
diff changeset
    40
42664
ae7707198403 simplified rail configuration;
wenzelm
parents: 42656
diff changeset
    41
\railtermfont{\isabellestyle{tt}}
55365
9d5aba2baa4c yet another attempt at actual underscore;
wenzelm
parents: 50109
diff changeset
    42
\railnontermfont{\isabellestyle{literalunderscore}}
9d5aba2baa4c yet another attempt at actual underscore;
wenzelm
parents: 50109
diff changeset
    43
\railnamefont{\isabellestyle{literalunderscore}}