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