changeset 55027 | a74ea6d75571 |
parent 55021 | e40090032de9 |
child 58127 | b7cab82f488e |
--- a/src/HOL/Cardinals/Order_Union.thy Fri Jan 17 10:02:49 2014 +0100 +++ b/src/HOL/Cardinals/Order_Union.thy Fri Jan 17 10:02:50 2014 +0100 @@ -7,7 +7,7 @@ header {* Order Union *} theory Order_Union -imports Wellfounded_More_FP +imports Order_Relation begin definition Osum :: "'a rel \<Rightarrow> 'a rel \<Rightarrow> 'a rel" (infix "Osum" 60) where