| author | Cezary Kaliszyk <kaliszyk@in.tum.de> |
| Fri, 12 Feb 2010 16:04:10 +0100 | |
| changeset 1139 | c4001cda9da3 |
| parent 1130 | fb5f5735a426 |
| child 1148 | 389d81959922 |
| permissions | -rw-r--r-- |
|
1130
fb5f5735a426
Added the missing syntax file
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
1 |
header {* Pretty syntax for Quotient operations *}
|
|
fb5f5735a426
Added the missing syntax file
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
2 |
|
|
fb5f5735a426
Added the missing syntax file
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
3 |
(*<*) |
|
fb5f5735a426
Added the missing syntax file
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
4 |
theory Quotient_Syntax |
|
fb5f5735a426
Added the missing syntax file
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
5 |
imports Quotient |
|
fb5f5735a426
Added the missing syntax file
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
6 |
begin |
|
fb5f5735a426
Added the missing syntax file
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
7 |
|
|
fb5f5735a426
Added the missing syntax file
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
8 |
notation |
|
fb5f5735a426
Added the missing syntax file
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
9 |
rel_conj (infixr "OOO" 75) and |
|
fb5f5735a426
Added the missing syntax file
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
10 |
fun_map (infixr "--->" 55) and |
|
fb5f5735a426
Added the missing syntax file
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
11 |
fun_rel (infixr "===>" 55) |
|
fb5f5735a426
Added the missing syntax file
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
12 |
|
|
fb5f5735a426
Added the missing syntax file
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
13 |
end |
|
fb5f5735a426
Added the missing syntax file
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
14 |
(*>*) |