--- a/Quotient-Paper-jv/document/root.tex	Wed Dec 21 17:05:00 2011 +0900
+++ b/Quotient-Paper-jv/document/root.tex	Thu Dec 22 04:46:37 2011 +0000
@@ -1,24 +1,22 @@
 \documentclass{svjour3}
-\usepackage{times}
-\usepackage{isabelle}
-\usepackage{isabellesym}
 \usepackage{amsmath}
 \usepackage{amssymb}
-\usepackage{pdfsetup}
+\usepackage{isabelle}
+\usepackage{isabellesym}
 \usepackage{tikz}
-%\usepackage{pgf}
+\usepackage{verbdef}
+\usepackage{mathpartir}
+\usepackage{pdfsetup}
+\usepackage{times}
 \usepackage{stmaryrd}
-\usepackage{verbdef}
-%\usepackage{longtable}
-\usepackage{mathpartir}
 %\newtheorem{definition}{Definition}
 %\newtheorem{proposition}{Proposition}
 %\newtheorem{lemma}{Lemma}
 
 \urlstyle{rm}
-\isabellestyle{rm}
-\renewcommand{\isastyleminor}{\rm}%
-\renewcommand{\isastyle}{\normalsize\rm}%
+\isabellestyle{it}
+\renewcommand{\isastyleminor}{\it}%
+\renewcommand{\isastyle}{\normalsize\it}%
 \renewcommand{\isastylescript}{\it}
 \def\dn{\,\triangleq\,}
 \verbdef\singlearr|---->|
@@ -29,6 +27,7 @@
 \renewcommand{\isasymemptyset}{$\varnothing$}
 %%\renewcommand{\isacharunderscore}{\mbox{$\_\!\_$}}
 \renewcommand{\isasymUnion}{$\bigcup$}
+\renewcommand{\isacharunderscore}{\text{$\_\!\_$}}
 
 \newcommand{\isasymsinglearr}{$\mapsto$}
 \newcommand{\isasymdoublearr}{$\Mapsto$}