| author | Cezary Kaliszyk <kaliszyk@in.tum.de> |
| Fri Feb 19 13:54:19 2010 +0100 (2010-02-19) | |
| changeset 35222 | 4f1fba00f66d |
| child 35787 | afdf1c4958b2 |
| permissions | -rw-r--r-- |
1 (* Title: Quotient_Syntax.thy
2 Author: Cezary Kaliszyk and Christian Urban
3 *)
5 header {* Pretty syntax for Quotient operations *}
7 (*<*)
8 theory Quotient_Syntax
9 imports Main
10 begin
12 notation
13 rel_conj (infixr "OOO" 75) and
14 fun_map (infixr "--->" 55) and
15 fun_rel (infixr "===>" 55)
17 end
18 (*>*)