# HG changeset patch
# User chaieb
# Date 1234199358 0
# Node ID 5ef75225c9c2153e08d4a4147e78c13582f3b61a
# Parent  4ac95212efcc2701efd24d92763b4542fd9d8f9e
added Euclidean_Space and Glbs to Library

diff -r 4ac95212efcc -r 5ef75225c9c2 src/HOL/IsaMakefile
--- a/src/HOL/IsaMakefile	Mon Feb 09 17:08:49 2009 +0000
+++ b/src/HOL/IsaMakefile	Mon Feb 09 17:09:18 2009 +0000
@@ -314,6 +314,7 @@
 $(LOG)/HOL-Library.gz: $(OUT)/HOL Library/SetsAndFunctions.thy		\
   Library/Abstract_Rat.thy \
   Library/BigO.thy Library/ContNotDenum.thy Library/Efficient_Nat.thy	\
+  Library/Euclidean_Space.thy Library/Glbs.thy Library/normarith.ML \
   Library/Executable_Set.thy Library/Infinite_Set.thy			\
   Library/FuncSet.thy \
   Library/Finite_Cartesian_Product.thy \
diff -r 4ac95212efcc -r 5ef75225c9c2 src/HOL/Library/Library.thy
--- a/src/HOL/Library/Library.thy	Mon Feb 09 17:08:49 2009 +0000
+++ b/src/HOL/Library/Library.thy	Mon Feb 09 17:09:18 2009 +0000
@@ -17,9 +17,9 @@
   Countable
   Efficient_Nat
   Enum
+  Euclidean_Space
   Eval_Witness
   Executable_Set
-  Finite_Cartesian_Product
   Float
   Formal_Power_Series
   FuncSet