# HG changeset patch # User chaieb # Date 1204119591 -3600 # Node ID 4d9d0a26c32a14b591162b364b4f4d9fd3174fa8 # Parent 420c1947511cfe10f7a0f5ae9597f974ba9e2763 Loads Dense_Linear_Order.thy diff -r 420c1947511c -r 4d9d0a26c32a src/HOL/Library/Library.thy --- a/src/HOL/Library/Library.thy Wed Feb 27 14:39:50 2008 +0100 +++ b/src/HOL/Library/Library.thy Wed Feb 27 14:39:51 2008 +0100 @@ -13,6 +13,7 @@ Coinductive_List Commutative_Ring Continuity + Dense_Linear_Order Efficient_Nat (*Eval*) Eval_Witness