equal
deleted
inserted
replaced
6 \usepackage{amsmath} |
6 \usepackage{amsmath} |
7 \usepackage{amssymb} |
7 \usepackage{amssymb} |
8 \usepackage{pdfsetup} |
8 \usepackage{pdfsetup} |
9 \usepackage{tikz} |
9 \usepackage{tikz} |
10 \usepackage{pgf} |
10 \usepackage{pgf} |
|
11 \usepackage{verbdef} |
11 |
12 |
12 \urlstyle{rm} |
13 \urlstyle{rm} |
13 \isabellestyle{it} |
14 \isabellestyle{it} |
14 \renewcommand{\isastyle}{\isastyleminor} |
15 \renewcommand{\isastyle}{\isastyleminor} |
15 |
16 |
16 \def\dn{\,\stackrel{\mbox{\scriptsize def}}{=}\,} |
17 \def\dn{\,\stackrel{\mbox{\scriptsize def}}{=}\,} |
|
18 \verbdef\singlearr|--->| |
|
19 \verbdef\doublearr|===>| |
|
20 |
17 \renewcommand{\isasymequiv}{$\dn$} |
21 \renewcommand{\isasymequiv}{$\dn$} |
18 \renewcommand{\isasymemptyset}{$\varnothing$} |
22 \renewcommand{\isasymemptyset}{$\varnothing$} |
19 \renewcommand{\isacharunderscore}{\mbox{$\_\!\_$}} |
23 \renewcommand{\isacharunderscore}{\mbox{$\_\!\_$}} |
20 \renewcommand{\isasymUnion}{$\bigcup$} |
24 \renewcommand{\isasymUnion}{$\bigcup$} |
|
25 |
|
26 \newcommand{\isasymsinglearr}{\singlearr} |
|
27 \newcommand{\isasymdoublearr}{\doublearr} |
|
28 |
21 \begin{document} |
29 \begin{document} |
22 |
30 |
23 \title{Quotients Revisited for Isabelle/HOL} |
31 \title{Quotients Revisited for Isabelle/HOL} |
24 \author{Cezary Kaliszyk$^*$ and Christian Urban$^*$} |
32 \author{Cezary Kaliszyk$^*$ and Christian Urban$^*$} |
25 \institute{$^*$ Technical University of Munich, Germany} |
33 \institute{$^*$ Technical University of Munich, Germany} |