# 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