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