| Mon, 14 May 2007 20:48:32 +0200 | huffman | add lemma sgn_mult; declare real_scaleR_def and scaleR_eq_0_iff as simp rules | changeset | files |
| Mon, 14 May 2007 20:14:31 +0200 | huffman | generalized sgn function to work on any real normed vector space | changeset | files |
| Mon, 14 May 2007 19:14:50 +0200 | huffman | root and sqrt on negative inputs | changeset | files |
| Mon, 14 May 2007 18:48:24 +0200 | huffman | move lemmas to RealPow.thy; tuned proofs | changeset | files |
| Mon, 14 May 2007 18:04:52 +0200 | huffman | tuned proofs | changeset | files |
| Mon, 14 May 2007 18:03:25 +0200 | huffman | tuned | changeset | files |
| Mon, 14 May 2007 17:45:42 +0200 | huffman | added general sum-squares lemmas | changeset | files |