# HG changeset patch
# User Cezary Kaliszyk <kaliszyk@in.tum.de>
# Date 1283151590 -32400
# Node ID 1b31d514a087921de5bf6f6d6dcbdb79dcf7fa86
# Parent  f89d1c52d647b56c1a91589870c64c33eec642ec# Parent  5e76af0a51f9fd1c42013ee8c11f3223a555b380
merge

diff -r 5e76af0a51f9 -r 1b31d514a087 Quotient-Paper/Paper.thy
--- a/Quotient-Paper/Paper.thy	Mon Aug 30 15:55:08 2010 +0900
+++ b/Quotient-Paper/Paper.thy	Mon Aug 30 15:59:50 2010 +0900
@@ -23,7 +23,7 @@
 notation (latex output)
   rel_conj ("_ \<circ>\<circ>\<circ> _" [53, 53] 52) and
   pred_comp ("_ \<circ>\<circ> _" [1, 1] 30) and
-  "op -->" (infix "\<longrightarrow>" 100) and
+  implies (infix "\<longrightarrow>" 100) and
   "==>" (infix "\<Longrightarrow>" 100) and
   fun_map ("_ \<singlearr> _" 51) and
   fun_rel ("_ \<doublearr> _" 51) and