| author | panny | 
| Wed, 18 Sep 2013 22:59:11 +0200 | |
| changeset 53720 | 03fac7082137 | 
| parent 50109 | c13dc0b1841c | 
| child 55365 | 9d5aba2baa4c | 
| permissions | -rw-r--r-- | 
| 
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 | 5  | 
\setcounter{secnumdepth}{2} \setcounter{tocdepth}{2}
 | 
6  | 
||
| 
26738
 
615e1a86787b
basic setup for generated document (cf. ../IsarImplementation);
 
wenzelm 
parents:  
diff
changeset
 | 
7  | 
%% references  | 
| 50109 | 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 | 11  | 
\newcommand{\Chref}[1]{Chapter~\ref{#1}}
 | 
12  | 
\newcommand{\appref}[1]{appendix~\ref{#1}}
 | 
|
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 | 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  | 
\isafoldtag{noproof}\def\isafoldnoproof{~\isafold{proof}}
 | 
| 
 
3b89d59a944b
accomodate digits within Isar command names, notably 'try0';
 
wenzelm 
parents: 
45646 
diff
changeset
 | 
20  | 
\newcommand{\isadigitreset}{\def\isadigit##1{##1}}
 | 
| 
 
3b89d59a944b
accomodate digits within Isar command names, notably 'try0';
 
wenzelm 
parents: 
45646 
diff
changeset
 | 
21  | 
\renewcommand{\isacommand}[1]{\isakeyword{\isadigitreset#1}}
 | 
| 
 
3b89d59a944b
accomodate digits within Isar command names, notably 'try0';
 
wenzelm 
parents: 
45646 
diff
changeset
 | 
22  | 
|
| 
28760
 
cbc435f7b16b
unified use of declaration environment with IsarImplementation;
 
wenzelm 
parents: 
28758 
diff
changeset
 | 
23  | 
%% ML  | 
| 
28763
 
b5e6122ff575
added pretty printing options (from old ref manual);
 
wenzelm 
parents: 
28760 
diff
changeset
 | 
24  | 
\newenvironment{mldecls}{\par\noindent\begingroup\def\isanewline{\\}\begin{tabular}{ll}}{\end{tabular}\medskip\endgroup}
 | 
| 28758 | 25  | 
|
| 
47586
 
3b89d59a944b
accomodate digits within Isar command names, notably 'try0';
 
wenzelm 
parents: 
45646 
diff
changeset
 | 
26  | 
\renewcommand{\isatagML}{\begingroup\isabellestyle{default}\isastyle\isadigitreset}
 | 
| 42654 | 27  | 
\renewcommand{\endisatagML}{\endgroup}
 | 
28  | 
||
| 26859 | 29  | 
%% math  | 
| 29725 | 30  | 
\newcommand{\isasymstrut}{\isamath{\mathstrut}}
 | 
31  | 
\newcommand{\isasymvartheta}{\isamath{\,\theta}}
 | 
|
| 26859 | 32  | 
\newcommand{\isactrlvec}[1]{\emph{$\overline{#1}$}}
 | 
33  | 
\renewcommand{\isadigit}[1]{\isamath{#1}}
 | 
|
| 29725 | 34  | 
\newcommand{\text}[1]{\mbox{#1}}
 | 
| 
26738
 
615e1a86787b
basic setup for generated document (cf. ../IsarImplementation);
 
wenzelm 
parents:  
diff
changeset
 | 
35  | 
|
| 26865 | 36  | 
%% global style options  | 
| 
26738
 
615e1a86787b
basic setup for generated document (cf. ../IsarImplementation);
 
wenzelm 
parents:  
diff
changeset
 | 
37  | 
\pagestyle{headings}
 | 
| 
 
615e1a86787b
basic setup for generated document (cf. ../IsarImplementation);
 
wenzelm 
parents:  
diff
changeset
 | 
38  | 
\sloppy  | 
| 
 
615e1a86787b
basic setup for generated document (cf. ../IsarImplementation);
 
wenzelm 
parents:  
diff
changeset
 | 
39  | 
|
| 42656 | 40  | 
\parindent 0pt\parskip 0.5ex  | 
41  | 
||
| 
45646
 
02afa20cf397
refined "literal" document style, with some correspondence to actual text source;
 
wenzelm 
parents: 
42666 
diff
changeset
 | 
42  | 
\isabellestyle{literal}
 | 
| 42631 | 43  | 
|
| 48579 | 44  | 
\newcommand{\isasymdash}{\isatext{\mbox{-}}}
 | 
45  | 
||
| 42664 | 46  | 
\railtermfont{\isabellestyle{tt}}
 | 
| 
45646
 
02afa20cf397
refined "literal" document style, with some correspondence to actual text source;
 
wenzelm 
parents: 
42666 
diff
changeset
 | 
47  | 
\railnontermfont{\isabellestyle{literal}}
 | 
| 
 
02afa20cf397
refined "literal" document style, with some correspondence to actual text source;
 
wenzelm 
parents: 
42666 
diff
changeset
 | 
48  | 
\railnamefont{\isabellestyle{literal}}
 |