equal
deleted
inserted
replaced
1 \documentclass{article} |
1 \documentclass{article} |
2 \newif\ifremarks |
2 \newif\ifremarks |
3 %\remarkstrue %TRUE causes remarks to be displayed (as marginal notes) |
3 \remarkstrue %TRUE causes remarks to be displayed (as marginal notes) |
4 \remarksfalse |
4 %\remarksfalse |
5 \usepackage{cl2emono-modified,isabelle,isabellesym} |
5 \usepackage{cl2emono-modified,isabelle,isabellesym} |
6 \usepackage{../proof,amsmath,amsfonts} |
6 \usepackage{../proof,amsmath,amsfonts} |
7 \usepackage{latexsym,verbatim,graphicx,../iman,../extra,../ttbox,comment} |
7 \usepackage{latexsym,verbatim,graphicx,../iman,../extra,../ttbox,comment} |
8 \usepackage{../pdfsetup} %last package! |
8 \usepackage{../pdfsetup} %last package! |
9 |
9 |
27 \renewenvironment{isamarkuptxt}{\begin{isamarkuptext}}{\end{isamarkuptext}} |
27 \renewenvironment{isamarkuptxt}{\begin{isamarkuptext}}{\end{isamarkuptext}} |
28 |
28 |
29 %% lcp's macros |
29 %% lcp's macros |
30 \newcommand{\REMARK}[1]{\ifremarks\marginpar{\raggedright\footnotesize#1}\fi} |
30 \newcommand{\REMARK}[1]{\ifremarks\marginpar{\raggedright\footnotesize#1}\fi} |
31 \newcommand{\rulename}[1]{\hfill$(\text{#1})$} %names of Isabelle rules |
31 \newcommand{\rulename}[1]{\hfill$(\text{#1})$} %names of Isabelle rules |
32 \let\bigisa=\isa |
|
33 %% was previously |
|
34 %% \newcommand{\bigisa}[1]{\texttt{\textsl{#1}}} |
|
35 %% because \isa is too small for variables, but does it really matter? |
|
36 |
|
37 |
32 |
38 %%% to index derived rls: ^\([a-zA-Z0-9][a-zA-Z0-9_]*\) \\tdx{\1} |
33 %%% to index derived rls: ^\([a-zA-Z0-9][a-zA-Z0-9_]*\) \\tdx{\1} |
39 %%% to index rulenames: ^ *(\([a-zA-Z0-9][a-zA-Z0-9_]*\), \\tdx{\1} |
34 %%% to index rulenames: ^ *(\([a-zA-Z0-9][a-zA-Z0-9_]*\), \\tdx{\1} |
40 %%% to index constants: \\tt \([a-zA-Z0-9][a-zA-Z0-9_]*\) \\cdx{\1} |
35 %%% to index constants: \\tt \([a-zA-Z0-9][a-zA-Z0-9_]*\) \\cdx{\1} |
41 %%% to deverbify: \\verb|\([^|]*\)| \\ttindex{\1} |
36 %%% to deverbify: \\verb|\([^|]*\)| \\ttindex{\1} |