Quot/Quotient.thy
changeset 1129 9a86f0ef6503
parent 1128 17ca92ab4660
child 1137 36d596cb63a2
--- a/Quot/Quotient.thy	Thu Feb 11 10:06:02 2010 +0100
+++ b/Quot/Quotient.thy	Thu Feb 11 14:00:00 2010 +0100
@@ -798,5 +798,10 @@
   {* Scan.succeed Quotient_Tacs.lifted_attrib *}
   {* lifts theorems to quotient types *}
 
+no_notation
+  rel_conj (infixr "OOO" 75) and
+  fun_map (infixr "--->" 55) and
+  fun_rel (infixr "===>" 55)
+
 end