src/HOL/Library/Order_Union.thy

--- a/src/HOL/Library/Order_Union.thy	Tue May 28 10:18:43 2013 +0200
+++ b/src/HOL/Library/Order_Union.thy	Tue May 28 13:19:51 2013 +0200
@@ -1,8 +1,7 @@
 (*  Title:      HOL/Library/Order_Union.thy
     Author:     Andrei Popescu, TU Muenchen
 
-Subset of Constructions_on_Wellorders that provides the ordinal sum but does
-not rely on the ~/HOL/Library/Zorn.thy.
+The ordinal-like sum of two orders with disjoint fields
 *)
 
 header {* Order Union *}