--- 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}