equal
deleted
inserted
replaced
11 \isabellestyle{it} |
11 \isabellestyle{it} |
12 \renewcommand{\isastyle}{\isastyleminor} |
12 \renewcommand{\isastyle}{\isastyleminor} |
13 |
13 |
14 \begin{document} |
14 \begin{document} |
15 |
15 |
16 \title{Quotients Revisited} |
16 \title{Quotients Revisited for Isabelle/HOL} |
17 \author{Cezary Kaliszyk$^*$ and Christian Urban$^*$} |
17 \author{Cezary Kaliszyk$^*$ and Christian Urban$^*$} |
18 \institute{$^*$ Technical University of Munich, Germany} |
18 \institute{$^*$ Technical University of Munich, Germany} |
19 \maketitle |
19 \maketitle |
20 |
20 |
21 \begin{abstract} |
21 \begin{abstract} |
22 TBD |
22 Higher-order logic (HOL) is based on a safe logic kernel, which |
|
23 can only be extended by introducing new definitions and new types. |
|
24 |
23 \end{abstract} |
25 \end{abstract} |
24 |
26 |
25 % generated text of all theories |
27 % generated text of all theories |
26 \input{session} |
28 \input{session} |
27 |
29 |