diff -r f89ee40fbb08 -r 78d828f43cdf Attic/Quot/Quotient_Syntax.thy
--- 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
-(*>*)