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