equal
deleted
inserted
replaced
5 *) |
5 *) |
6 |
6 |
7 section \<open>Order Union\<close> |
7 section \<open>Order Union\<close> |
8 |
8 |
9 theory Order_Union |
9 theory Order_Union |
10 imports Order_Relation |
10 imports HOL.Order_Relation |
11 begin |
11 begin |
12 |
12 |
13 definition Osum :: "'a rel \<Rightarrow> 'a rel \<Rightarrow> 'a rel" (infix "Osum" 60) where |
13 definition Osum :: "'a rel \<Rightarrow> 'a rel \<Rightarrow> 'a rel" (infix "Osum" 60) where |
14 "r Osum r' = r \<union> r' \<union> {(a, a'). a \<in> Field r \<and> a' \<in> Field r'}" |
14 "r Osum r' = r \<union> r' \<union> {(a, a'). a \<in> Field r \<and> a' \<in> Field r'}" |
15 |
15 |