branch | Nominal2-Isabelle2012 |
changeset 3169 | b6873d123f9b |
parent 3168 | a6f3e1b08494 |
child 3170 | 89715c48f728 |
--- a/Attic/Quot/Quotient_Syntax.thy Sat May 12 21:05:59 2012 +0100 +++ /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 -(*>*)