equal
deleted
inserted
replaced
12 %%% to index derived rls: ^\([a-zA-Z0-9][a-zA-Z0-9_]*\) \\tdx{\1} |
12 %%% to index derived rls: ^\([a-zA-Z0-9][a-zA-Z0-9_]*\) \\tdx{\1} |
13 %%% to index rulenames: ^ *(\([a-zA-Z0-9][a-zA-Z0-9_]*\), \\tdx{\1} |
13 %%% to index rulenames: ^ *(\([a-zA-Z0-9][a-zA-Z0-9_]*\), \\tdx{\1} |
14 %%% to index constants: \\tt \([a-zA-Z0-9][a-zA-Z0-9_]*\) \\cdx{\1} |
14 %%% to index constants: \\tt \([a-zA-Z0-9][a-zA-Z0-9_]*\) \\cdx{\1} |
15 %%% to deverbify: \\verb|\([^|]*\)| \\ttindex{\1} |
15 %%% to deverbify: \\verb|\([^|]*\)| \\ttindex{\1} |
16 |
16 |
17 \title{\includegraphics[scale=0.5]{isabelle_hol.eps} \\[4ex] |
17 \title{\includegraphics[scale=0.5]{isabelle_hol} \\[4ex] |
18 Isabelle's Logics: HOL} |
18 Isabelle's Logics: HOL} |
19 |
19 |
20 \author{Tobias Nipkow\footnote |
20 \author{Tobias Nipkow\footnote |
21 {Institut f\"ur Informatik, Technische Universit\"at M\"unchen, |
21 {Institut f\"ur Informatik, Technische Universit\"at M\"unchen, |
22 \texttt{nipkow@in.tum.de}}, |
22 \texttt{nipkow@in.tum.de}}, |
54 Isabelle/HOL, and the \emph{Isabelle Reference Manual} for general Isabelle |
54 Isabelle/HOL, and the \emph{Isabelle Reference Manual} for general Isabelle |
55 commands. |
55 commands. |
56 \end{abstract} |
56 \end{abstract} |
57 |
57 |
58 \pagenumbering{roman} \tableofcontents \clearfirst |
58 \pagenumbering{roman} \tableofcontents \clearfirst |
59 \include{../Logics/syntax} |
59 \input{../Logics/syntax} |
60 \include{HOL} |
60 \include{HOL} |
61 \bibliographystyle{plain} |
61 \bibliographystyle{plain} |
62 \bibliography{../manual} |
62 \bibliography{../manual} |
63 \input{logics-HOL.ind} |
63 \input{logics-HOL.ind} |
64 \end{document} |
64 \end{document} |