diff -r fb201e383f1b -r da575186d492 Attic/Quot/Quotient_Syntax.thy --- 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 -(*>*)