# HG changeset patch
# User urbanc
# Date 1296408113 0
# Node ID 4a517c6ac07d2dac34f7ab72b86f8e9a00a2cbd9
# Parent  6cfb92de46542274a189defe75e83bfa8e3ab0c6
tuning of the syntax; needs the stmaryrd latex package

diff -r 6cfb92de4654 -r 4a517c6ac07d Paper/Paper.thy
--- 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)
+
 
 (*>*)
 
diff -r 6cfb92de4654 -r 4a517c6ac07d Paper/document/root.tex
--- 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}