--- a/Paper/Paper.thy	Sun Jan 30 17:09:02 2011 +0000
+++ b/Paper/Paper.thy	Sun Jan 30 17:21:53 2011 +0000
@@ -10,7 +10,9 @@
   Seq (infixr "\<cdot>" 100) and
   Star ("_\<^bsup>\<star>\<^esup>") and
   pow ("_\<^bsup>_\<^esup>" [100, 100] 100) and
-  Suc ("_+1" [100] 100)
+  Suc ("_+1" [100] 100) and
+  quotient ("_ \<^raw:\ensuremath{\sslash}> _ " [90, 90] 90)
+
 
 (*>*)
 

--- a/Paper/document/root.tex	Sun Jan 30 17:09:02 2011 +0000
+++ b/Paper/document/root.tex	Sun Jan 30 17:21:53 2011 +0000
@@ -9,7 +9,7 @@
 \usepackage{ot1patch}
 \usepackage{times}
 \usepackage{proof}
-
+\usepackage{stmaryrd}
 
 \urlstyle{rm}
 \isabellestyle{it}