diff -r 7a6b87adebc8 -r 66ef2a2c64fb Pearl-jv/document/root.tex
--- a/Pearl-jv/document/root.tex	Wed Apr 13 13:44:25 2011 +0100
+++ b/Pearl-jv/document/root.tex	Fri Apr 22 00:18:25 2011 +0800
@@ -4,6 +4,7 @@
 \usepackage{isabellesym}
 \usepackage{amsmath}
 \usepackage{amssymb}
+\usepackage{mathabx}
 \usepackage{longtable}
 \usepackage{graphics}
 \usepackage{pdfsetup}
@@ -19,10 +20,13 @@
 \renewcommand{\isasymrightleftharpoons}{}
 \renewcommand{\isasymemptyset}{$\varnothing$}
 \newcommand{\isasymallatoms}{\ensuremath{\mathbb{A}}}
+\newcommand{\rrh}{\mbox{\footnotesize$\rightrightharpoons$}}
 
 \newcommand{\numbered}[1]{\refstepcounter{equation}{\rm(\arabic{equation})}\label{#1}}
 \newcommand\new[0]{\reflectbox{\ensuremath{\mathsf{N}}}}
 
+\changenotsign
+
 \begin{document}
 
 \title{Implementing the Nominal Logic Work in Isabelle/HOL}