branch | Nominal2-Isabelle2013 |
changeset 3208 | da575186d492 |
parent 3206 | fb201e383f1b |
child 3209 | 2fb0bc0dcbf1 |
3206:fb201e383f1b | 3208:da575186d492 |
---|---|
1 (* Title: Quotient_Syntax.thy |
|
2 Author: Cezary Kaliszyk and Christian Urban |
|
3 *) |
|
4 |
|
5 header {* Pretty syntax for Quotient operations *} |
|
6 |
|
7 (*<*) |
|
8 theory Quotient_Syntax |
|
9 imports Quotient |
|
10 begin |
|
11 |
|
12 notation |
|
13 rel_conj (infixr "OOO" 75) and |
|
14 fun_map (infixr "--->" 55) and |
|
15 fun_rel (infixr "===>" 55) |
|
16 |
|
17 end |
|
18 (*>*) |