Quotient-Paper/document/root.tex
changeset 2224 f5b6f9d8a882
parent 2223 c474186439bd
child 2226 36c9d9e658c7
equal deleted inserted replaced
2223:c474186439bd 2224:f5b6f9d8a882
    14 \renewcommand{\isastyle}{\isastyleminor}
    14 \renewcommand{\isastyle}{\isastyleminor}
    15 
    15 
    16 \def\dn{\,\stackrel{\mbox{\scriptsize def}}{=}\,}
    16 \def\dn{\,\stackrel{\mbox{\scriptsize def}}{=}\,}
    17 \renewcommand{\isasymequiv}{$\dn$}
    17 \renewcommand{\isasymequiv}{$\dn$}
    18 \renewcommand{\isasymemptyset}{$\varnothing$}
    18 \renewcommand{\isasymemptyset}{$\varnothing$}
    19 
    19 \renewcommand{\isacharunderscore}{\mbox{$\_\!\_$}}
       
    20 \renewcommand{\isasymUnion}{$\bigcup$}
    20 \begin{document}
    21 \begin{document}
    21 
    22 
    22 \title{Quotients Revisited for Isabelle/HOL}
    23 \title{Quotients Revisited for Isabelle/HOL}
    23 \author{Cezary Kaliszyk$^*$ and Christian Urban$^*$}
    24 \author{Cezary Kaliszyk$^*$ and Christian Urban$^*$}
    24 \institute{$^*$ Technical University of Munich, Germany}
    25 \institute{$^*$ Technical University of Munich, Germany}