# HG changeset patch # User wenzelm # Date 1204153888 -3600 # Node ID 5cac519abe4ee424a4fe257f9398b2d83a7d64f4 # Parent fa302c5bc2f2d334f04e1c2ed663a0b3ec18bd74 renamed ListSpace to ListVector; diff -r fa302c5bc2f2 -r 5cac519abe4e src/HOL/Library/Library.thy --- a/src/HOL/Library/Library.thy Thu Feb 28 00:04:47 2008 +0100 +++ b/src/HOL/Library/Library.thy Thu Feb 28 00:11:28 2008 +0100 @@ -25,7 +25,7 @@ GCD Imperative_HOL Infinite_Set - ListSpace + ListVector Multiset NatPair Nat_Infinity