added Euclidean_Space and Glbs to Library
authorchaieb
Mon Feb 09 17:09:18 2009 +0000 (2009-02-09)
changeset 298455ef75225c9c2
parent 29844 4ac95212efcc
child 29846 57dccccc37b3
added Euclidean_Space and Glbs to Library
src/HOL/IsaMakefile
src/HOL/Library/Library.thy
     1.1 --- a/src/HOL/IsaMakefile	Mon Feb 09 17:08:49 2009 +0000
     1.2 +++ b/src/HOL/IsaMakefile	Mon Feb 09 17:09:18 2009 +0000
     1.3 @@ -314,6 +314,7 @@
     1.4  $(LOG)/HOL-Library.gz: $(OUT)/HOL Library/SetsAndFunctions.thy		\
     1.5    Library/Abstract_Rat.thy \
     1.6    Library/BigO.thy Library/ContNotDenum.thy Library/Efficient_Nat.thy	\
     1.7 +  Library/Euclidean_Space.thy Library/Glbs.thy Library/normarith.ML \
     1.8    Library/Executable_Set.thy Library/Infinite_Set.thy			\
     1.9    Library/FuncSet.thy \
    1.10    Library/Finite_Cartesian_Product.thy \
     2.1 --- a/src/HOL/Library/Library.thy	Mon Feb 09 17:08:49 2009 +0000
     2.2 +++ b/src/HOL/Library/Library.thy	Mon Feb 09 17:09:18 2009 +0000
     2.3 @@ -17,9 +17,9 @@
     2.4    Countable
     2.5    Efficient_Nat
     2.6    Enum
     2.7 +  Euclidean_Space
     2.8    Eval_Witness
     2.9    Executable_Set
    2.10 -  Finite_Cartesian_Product
    2.11    Float
    2.12    Formal_Power_Series
    2.13    FuncSet