# HG changeset patch
# User wenzelm
# Date 1369686607 -7200
# Node ID 636b62eb7e88d8bdf5632faa11e726a284077d7d
# Parent  c87b7f26e2c73cbbb41bc7b98ca72e8c2c6ac9cc
more direct notation;

diff -r c87b7f26e2c7 -r 636b62eb7e88 src/HOL/Library/Order_Union.thy
--- a/src/HOL/Library/Order_Union.thy	Mon May 27 22:26:08 2013 +0200
+++ b/src/HOL/Library/Order_Union.thy	Mon May 27 22:30:07 2013 +0200
@@ -14,8 +14,7 @@
 definition Osum :: "'a rel \<Rightarrow> 'a rel \<Rightarrow> 'a rel"  (infix "Osum" 60) where
   "r Osum r' = r \<union> r' \<union> {(a, a'). a \<in> Field r \<and> a' \<in> Field r'}"
 
-abbreviation Osum2 :: "'a rel \<Rightarrow> 'a rel \<Rightarrow> 'a rel" (infix "\<union>o" 60) where
-  "r \<union>o r' \<equiv> r Osum r'"
+notation Osum  (infix "\<union>o" 60)
 
 lemma Field_Osum: "Field (r \<union>o r') = Field r \<union> Field r'"
   unfolding Osum_def Field_def by blast