src/HOL/Library/Euclidean_Space.thy
Wed, 04 Mar 2009 19:21:56 +0000 chaieb fixed proofs; added rules as default simp-rules
Wed, 04 Mar 2009 11:05:29 +0100 blanchet Merge.
Wed, 04 Mar 2009 10:45:52 +0100 blanchet Merge.
Sun, 22 Feb 2009 08:52:44 -0800 huffman remove duplicate instance declaration
Sat, 21 Feb 2009 15:39:59 -0800 huffman real_inner class instance for vectors
Sat, 21 Feb 2009 11:18:50 -0800 huffman remove duplicated lemmas about norm
Sat, 21 Feb 2009 10:58:25 -0800 huffman real_normed_vector instance
Sat, 21 Feb 2009 09:55:32 -0800 huffman fix real_vector, real_algebra instances
Fri, 13 Feb 2009 14:45:10 -0800 huffman section -> subsection
Fri, 13 Feb 2009 14:41:54 -0800 huffman add instance for cancel_comm_monoid_add
Thu, 12 Feb 2009 12:35:45 -0800 huffman fix document generation
Mon, 09 Feb 2009 17:08:49 +0000 chaieb fixed proof -- removed unnecessary sorry
Mon, 09 Feb 2009 16:54:03 +0000 chaieb (Real) Vectors in Euclidean space, and elementary linear algebra.
less more (0) tip