--- a/Quotient-Paper-jv/Paper.thy	Wed Dec 21 17:05:00 2011 +0900
+++ b/Quotient-Paper-jv/Paper.thy	Thu Dec 22 04:46:37 2011 +0000
@@ -165,6 +165,9 @@
   makes the formal
   proof of the substitution lemma almost trivial.
 
+  {\bf MAYBE AN EAMPLE FOR PARTIAL QUOTIENTS?}
+
+
   The difficulty is that in order to be able to reason about integers, finite
   sets or $\alpha$-equated lambda-terms one needs to establish a reasoning
   infrastructure by transferring, or \emph{lifting}, definitions and theorems
@@ -331,7 +334,7 @@
   package works in practise.
 *}
 
-section {* Preliminaries and General\\ Quotients\label{sec:prelims} *}
+section {* Preliminaries and General Quotients\label{sec:prelims} *}
 
 text {*
   \noindent
@@ -498,7 +501,7 @@
   \end{isabelle}
 *}
 
-section {* Quotient Types and Quotient\\ Definitions\label{sec:type} *}
+section {* Quotient Types and Quotient Definitions\label{sec:type} *}
 
 text {*
   \noindent
@@ -758,7 +761,7 @@
   \end{proof}
 *}
 
-section {* Respectfulness and\\ Preservation \label{sec:resp} *}
+section {* Respectfulness and Preservation \label{sec:resp} *}
 
 text {*
   \noindent

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