| author | blanchet |
| Wed Sep 24 15:45:55 2014 +0200 (2014-09-24) | |
| changeset 58425 | 246985c6b20b |
| parent 55945 | e96383acecf9 |
| child 58881 | b9556a055632 |
| permissions | -rw-r--r-- |
1 (* Title: HOL/Library/Quotient_Syntax.thy
2 Author: Cezary Kaliszyk and Christian Urban
3 *)
5 header {* Pretty syntax for Quotient operations *}
7 theory Quotient_Syntax
8 imports Main
9 begin
11 notation
12 rel_conj (infixr "OOO" 75) and
13 map_fun (infixr "--->" 55) and
14 rel_fun (infixr "===>" 55)
16 end