equal
deleted
inserted
replaced
14 %%% to index derived rls: ^\([a-zA-Z0-9][a-zA-Z0-9_]*\) \\tdx{\1} |
14 %%% to index derived rls: ^\([a-zA-Z0-9][a-zA-Z0-9_]*\) \\tdx{\1} |
15 %%% to index rulenames: ^ *(\([a-zA-Z0-9][a-zA-Z0-9_]*\), \\tdx{\1} |
15 %%% to index rulenames: ^ *(\([a-zA-Z0-9][a-zA-Z0-9_]*\), \\tdx{\1} |
16 %%% to index constants: \\tt \([a-zA-Z0-9][a-zA-Z0-9_]*\) \\cdx{\1} |
16 %%% to index constants: \\tt \([a-zA-Z0-9][a-zA-Z0-9_]*\) \\cdx{\1} |
17 %%% to deverbify: \\verb|\([^|]*\)| \\ttindex{\1} |
17 %%% to deverbify: \\verb|\([^|]*\)| \\ttindex{\1} |
18 %% run ../sedindex logics to prepare index file |
18 %% run ../sedindex logics to prepare index file |
19 \title{\includegraphics[scale=0.5]{../isabelle.ps} \\[4ex] Isabelle's Object-Logics} |
19 \title{\includegraphics[scale=0.5]{../isabelle.eps} \\[4ex] Isabelle's Object-Logics} |
20 |
20 |
21 \author{{\em Lawrence C. Paulson}\\ |
21 \author{{\em Lawrence C. Paulson}\\ |
22 Computer Laboratory \\ University of Cambridge \\ |
22 Computer Laboratory \\ University of Cambridge \\ |
23 \texttt{lcp@cl.cam.ac.uk}\\[3ex] |
23 \texttt{lcp@cl.cam.ac.uk}\\[3ex] |
24 With Contributions by Tobias Nipkow and Markus Wenzel% |
24 With Contributions by Tobias Nipkow and Markus Wenzel% |