branch | Nominal2-Isabelle2011-1 |
changeset 3069 | 78d828f43cdf |
parent 3068 | f89ee40fbb08 |
child 3070 | 4b4742aa43f2 |
--- a/Attic/Quot/Quotient_Syntax.thy Sat Dec 17 16:57:25 2011 +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 -(*>*)