--- a/Quotient-Paper/document/root.tex	Fri Aug 27 16:00:19 2010 +0800
+++ b/Quotient-Paper/document/root.tex	Fri Aug 27 19:06:30 2010 +0800
@@ -9,6 +9,7 @@
 \usepackage{pdfsetup}
 \usepackage{tikz}
 \usepackage{pgf}
+\usepackage{stmaryrd}
 \usepackage{verbdef}
 \usepackage{longtable}
 \usepackage{mathpartir}
@@ -20,9 +21,9 @@
 \isabellestyle{rm}
 \renewcommand{\isastyleminor}{\rm}%
 \renewcommand{\isastyle}{\normalsize\rm}%
-
-\def\dn{\,\stackrel{\mbox{\scriptsize def}}{=}\,}
-\verbdef\singlearr|--->|
+\renewcommand{\isastylescript}{\it}
+\def\dn{\,\triangleq\,}
+\verbdef\singlearr|---->|
 \verbdef\doublearr|===>|
 \verbdef\tripple|###|
 
@@ -31,8 +32,8 @@
 %%\renewcommand{\isacharunderscore}{\mbox{$\_\!\_$}}
 \renewcommand{\isasymUnion}{$\bigcup$}
 
-\newcommand{\isasymsinglearr}{\singlearr}
-\newcommand{\isasymdoublearr}{\doublearr}
+\newcommand{\isasymsinglearr}{$\mapsto$}
+\newcommand{\isasymdoublearr}{$\Mapsto$}
 \newcommand{\isasymtripple}{\tripple}
 
 \newcommand{\numbered}[1]{\refstepcounter{equation}{\rm(\arabic{equation})}\label{#1}}