changeset 23854 | 688a8a7bcd4e |
parent 23192 | ec73b9707d48 |
child 24197 | c9e3cb5e5681 |
--- a/src/HOL/Library/Library.thy Thu Jul 19 21:47:38 2007 +0200 +++ b/src/HOL/Library/Library.thy Thu Jul 19 21:47:39 2007 +0200 @@ -9,15 +9,15 @@ Coinductive_List Commutative_Ring Continuity - EfficientNat + Efficient_Nat Eval - ExecutableRat + Executable_Rat Executable_Real - ExecutableSet + Executable_Set FuncSet GCD Infinite_Set - MLString + ML_String Multiset NatPair Nat_Infinity