src/HOL/Real/RealVector.thy
Sat, 16 Sep 2006 19:12:03 +0200 huffman define new constant of_real for class real_algebra_1;
Sat, 16 Sep 2006 02:35:58 +0200 huffman add theorem norm_diff_triangle_ineq
Thu, 14 Sep 2006 03:25:17 +0200 huffman remove conflicting norm syntax
Tue, 12 Sep 2006 06:44:45 +0200 huffman formalization of vector spaces and algebras over the real numbers
less more (0) tip