equal
deleted
inserted
replaced
1 (* Title: Quotient_Syntax.thy |
1 (* Title: HOL/Library/Quotient_Syntax.thy |
2 Author: Cezary Kaliszyk and Christian Urban |
2 Author: Cezary Kaliszyk and Christian Urban |
3 *) |
3 *) |
4 |
4 |
5 header {* Pretty syntax for Quotient operations *} |
5 header {* Pretty syntax for Quotient operations *} |
6 |
6 |
7 (*<*) |
|
8 theory Quotient_Syntax |
7 theory Quotient_Syntax |
9 imports Main |
8 imports Main |
10 begin |
9 begin |
11 |
10 |
12 notation |
11 notation |
13 rel_conj (infixr "OOO" 75) and |
12 rel_conj (infixr "OOO" 75) and |
14 fun_map (infixr "--->" 55) and |
13 fun_map (infixr "--->" 55) and |
15 fun_rel (infixr "===>" 55) |
14 fun_rel (infixr "===>" 55) |
16 |
15 |
17 end |
16 end |
18 (*>*) |
|