changeset 1260 | 9df6144e281b |
parent 1148 | 389d81959922 |
--- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/Attic/Quot/Quotient_Syntax.thy Thu Feb 25 07:57:17 2010 +0100 @@ -0,0 +1,18 @@ +(* Title: Quotient_Syntax.thy + Author: Cezary Kaliszyk and Christian Urban +*) + +header {* Pretty syntax for Quotient operations *} + +(*<*) +theory Quotient_Syntax +imports Quotient +begin + +notation + rel_conj (infixr "OOO" 75) and + fun_map (infixr "--->" 55) and + fun_rel (infixr "===>" 55) + +end +(*>*)