diff -r d40031f786f0 -r 72ce58b76c3b Quotient-Paper/document/root.tex --- a/Quotient-Paper/document/root.tex Mon Jun 14 19:03:34 2010 +0200 +++ b/Quotient-Paper/document/root.tex Tue Jun 15 02:03:18 2010 +0200 @@ -10,6 +10,7 @@ \usepackage{pgf} \usepackage{verbdef} \usepackage{longtable} +\usepackage{mathpartir} \urlstyle{rm} \isabellestyle{it} @@ -18,6 +19,7 @@ \def\dn{\,\stackrel{\mbox{\scriptsize def}}{=}\,} \verbdef\singlearr|--->| \verbdef\doublearr|===>| +\verbdef\tripple|###| \renewcommand{\isasymequiv}{$\dn$} \renewcommand{\isasymemptyset}{$\varnothing$} @@ -26,8 +28,10 @@ \newcommand{\isasymsinglearr}{\singlearr} \newcommand{\isasymdoublearr}{\doublearr} +\newcommand{\isasymtripple}{\tripple} \newcommand{\numbered}[1]{\refstepcounter{equation}{\rm(\arabic{equation})}\label{#1}} + \begin{document} \title{Quotients Revisited for Isabelle/HOL}