8 \usepackage{pdfsetup} |
8 \usepackage{pdfsetup} |
9 \usepackage{tikz} |
9 \usepackage{tikz} |
10 \usepackage{pgf} |
10 \usepackage{pgf} |
11 \usepackage{verbdef} |
11 \usepackage{verbdef} |
12 \usepackage{longtable} |
12 \usepackage{longtable} |
|
13 \usepackage{mathpartir} |
13 |
14 |
14 \urlstyle{rm} |
15 \urlstyle{rm} |
15 \isabellestyle{it} |
16 \isabellestyle{it} |
16 \renewcommand{\isastyle}{\isastyleminor} |
17 \renewcommand{\isastyle}{\isastyleminor} |
17 |
18 |
18 \def\dn{\,\stackrel{\mbox{\scriptsize def}}{=}\,} |
19 \def\dn{\,\stackrel{\mbox{\scriptsize def}}{=}\,} |
19 \verbdef\singlearr|--->| |
20 \verbdef\singlearr|--->| |
20 \verbdef\doublearr|===>| |
21 \verbdef\doublearr|===>| |
|
22 \verbdef\tripple|###| |
21 |
23 |
22 \renewcommand{\isasymequiv}{$\dn$} |
24 \renewcommand{\isasymequiv}{$\dn$} |
23 \renewcommand{\isasymemptyset}{$\varnothing$} |
25 \renewcommand{\isasymemptyset}{$\varnothing$} |
24 \renewcommand{\isacharunderscore}{\mbox{$\_\!\_$}} |
26 \renewcommand{\isacharunderscore}{\mbox{$\_\!\_$}} |
25 \renewcommand{\isasymUnion}{$\bigcup$} |
27 \renewcommand{\isasymUnion}{$\bigcup$} |
26 |
28 |
27 \newcommand{\isasymsinglearr}{\singlearr} |
29 \newcommand{\isasymsinglearr}{\singlearr} |
28 \newcommand{\isasymdoublearr}{\doublearr} |
30 \newcommand{\isasymdoublearr}{\doublearr} |
|
31 \newcommand{\isasymtripple}{\tripple} |
29 |
32 |
30 \newcommand{\numbered}[1]{\refstepcounter{equation}{\rm(\arabic{equation})}\label{#1}} |
33 \newcommand{\numbered}[1]{\refstepcounter{equation}{\rm(\arabic{equation})}\label{#1}} |
|
34 |
31 \begin{document} |
35 \begin{document} |
32 |
36 |
33 \title{Quotients Revisited for Isabelle/HOL} |
37 \title{Quotients Revisited for Isabelle/HOL} |
34 \author{Cezary Kaliszyk$^*$ and Christian Urban$^*$} |
38 \author{Cezary Kaliszyk$^*$ and Christian Urban$^*$} |
35 \institute{$^*$ Technical University of Munich, Germany} |
39 \institute{$^*$ Technical University of Munich, Germany} |