diff -r 1f9360daf6e1 -r 5606de1e5034 Quotient-Paper/document/root.tex
--- a/Quotient-Paper/document/root.tex	Fri Aug 27 13:57:00 2010 +0800
+++ b/Quotient-Paper/document/root.tex	Fri Aug 27 16:00:19 2010 +0800
@@ -17,8 +17,8 @@
 \newtheorem{lemma}{Lemma}
 
 \urlstyle{rm}
-\isabellestyle{it}
-\renewcommand{\isastyleminor}{\it}%
+\isabellestyle{rm}
+\renewcommand{\isastyleminor}{\rm}%
 \renewcommand{\isastyle}{\normalsize\rm}%
 
 \def\dn{\,\stackrel{\mbox{\scriptsize def}}{=}\,}
@@ -26,9 +26,9 @@
 \verbdef\doublearr|===>|
 \verbdef\tripple|###|
 
-\renewcommand{\isasymequiv}{$\dn$}
+\renewcommand{\isasymequiv}{$\triangleq$}
 \renewcommand{\isasymemptyset}{$\varnothing$}
-\renewcommand{\isacharunderscore}{\mbox{$\_\!\_$}}
+%%\renewcommand{\isacharunderscore}{\mbox{$\_\!\_$}}
 \renewcommand{\isasymUnion}{$\bigcup$}
 
 \newcommand{\isasymsinglearr}{\singlearr}
@@ -63,19 +63,18 @@
 mechanism for extension is the introduction of safe definitions and of
 non-empty types. Both extensions are often performed in quotient
 constructions. To ease the work involved with such quotient constructions, we
-re-implemented in Isabelle/HOL the quotient package by Homeier. In doing so we
-extended his work in order to deal with compositions of quotients. Like his
-package, we designed our quotient package so that every step in a quotient construction
-can be performed separately and as a result we are able to specify completely
-the procedure of lifting theorems from the raw level to the quotient level.
-The importance for programming language research is that many properties of
-programming language calculi are easier to verify over $\alpha$-equated, or
-$\alpha$-quotient, terms, than over raw terms.
+re-implemented in the popular Isabelle/HOL theorem prover the quotient 
+package by Homeier. In doing so we extended his work in order to deal with 
+compositions of quotients and we are also able to specify completely the procedure 
+of lifting theorems from the raw level to the quotient level.
+The importance for theorem proving is that many formal
+verifications, in order to be feasible, require a convenient resoning infrastructure 
+for quotient constructions.
 \end{abstract}
 
-\category{D.??}{TODO}{TODO}
+%\category{D.??}{TODO}{TODO}
 
-\keywords{quotients, isabelle, higher order logic}
+\keywords{Quotients, Isabelle theorem prover, Higher-Order Logic}
 
 % generated text of all theories
 \input{session}