branch | Nominal2-Isabelle2013 |
changeset 3208 | da575186d492 |
parent 3206 | fb201e383f1b |
child 3209 | 2fb0bc0dcbf1 |
--- a/Attic/Quot/Quotient_Syntax.thy Tue Feb 19 05:38:46 2013 +0000 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,18 +0,0 @@ -(* 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 -(*>*)