Attic/Quot/Quotient_Syntax.thy
branchNominal2-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
-(*>*)