2009-02-09 nipkow [Mon, 09 Feb 2009 22:15:37 +0100] rev 29851
merged

2009-02-09 nipkow [Mon, 09 Feb 2009 22:14:33 +0100] rev 29850
fix to [arith]
src/HOL/Tools/lin_arith.ML

2009-02-09 nipkow [Mon, 09 Feb 2009 18:50:10 +0100] rev 29849
new attribute "arith" for facts supplied to arith.
src/HOL/Nat.thy src/HOL/Tools/lin_arith.ML

2009-02-09 Timothy Bourke [Mon, 09 Feb 2009 17:25:07 +1100] rev 29848
Nicer names in FindTheorems.
* Patch NameSpace.get_accesses, contributed by Timothy Bourke:

NameSpace.get_accesses has been patched to fix the following
bug:
theory OverHOL imports Main begin
lemma conjI: "a & b --> b"
by blast

ML {* val ns = PureThy.facts_of @{theory} |> Facts.space_of;
val x1 = NameSpace.get_accesses ns "HOL.conjI";
val x2 = NameSpace.get_accesses ns "OverHOL.conjI"; *}
end

where x1 = ["conjI", "HOL.conjI"] and x2 = ["conjI", "OverHOL.conjI"],
but x1 should be just ["HOL.conjI"].

NameSpace.get_accesses is only used within the NameSpace
structure itself. The two uses have been modified to retain
their original behaviour.

Note that NameSpace.valid_accesses gives different results:
get_accesses ns "HOL.eq_class.eq"
gives ["eq", "eq_class.eq", "HOL.eq_class.eq"]
but,
valid_accesses ns "HOL.eq_class.eq"
gives ["HOL.eq_class.eq", "eq_class.eq", "HOL.eq", "eq"]

* Patch FindTheorems:
Prefer names that are shorter to type in the current context.

* Re-export space_of.
src/Pure/General/name_space.ML src/Pure/Isar/find_theorems.ML src/Pure/facts.ML

2009-02-09 chaieb [Mon, 09 Feb 2009 17:21:46 +0000] rev 29847
added Determinants to Library
src/HOL/IsaMakefile src/HOL/Library/Library.thy

2009-02-09 chaieb [Mon, 09 Feb 2009 17:21:19 +0000] rev 29846
Traces, Determinant of square matrices and some properties
src/HOL/Library/Determinants.thy

2009-02-09 chaieb [Mon, 09 Feb 2009 17:09:18 +0000] rev 29845
added Euclidean_Space and Glbs to Library
src/HOL/IsaMakefile src/HOL/Library/Library.thy

2009-02-09 chaieb [Mon, 09 Feb 2009 17:08:49 +0000] rev 29844
fixed proof -- removed unnecessary sorry
src/HOL/Library/Euclidean_Space.thy

2009-02-09 chaieb [Mon, 09 Feb 2009 16:57:10 +0000] rev 29843
Fixed theorem reference
src/HOL/Library/normarith.ML

2009-02-09 chaieb [Mon, 09 Feb 2009 16:54:03 +0000] rev 29842
(Real) Vectors in Euclidean space, and elementary linear algebra.
src/HOL/Library/Euclidean_Space.thy