isabelle: Changelog

huffman [Mon, 14 May 2007 20:48:32 +0200] rev 22973

add lemma sgn_mult; declare real_scaleR_def and scaleR_eq_0_iff as simp rules

huffman [Mon, 14 May 2007 20:14:31 +0200] rev 22972

generalized sgn function to work on any real normed vector space

huffman [Mon, 14 May 2007 19:14:50 +0200] rev 22971

root and sqrt on negative inputs

huffman [Mon, 14 May 2007 18:48:24 +0200] rev 22970

move lemmas to RealPow.thy; tuned proofs

huffman [Mon, 14 May 2007 18:04:52 +0200] rev 22969

tuned proofs

huffman [Mon, 14 May 2007 18:03:25 +0200] rev 22968

tuned

huffman [Mon, 14 May 2007 17:45:42 +0200] rev 22967

added general sum-squares lemmas

huffman [Mon, 14 May 2007 17:37:31 +0200] rev 22966

new lemmas

webertj [Mon, 14 May 2007 13:24:22 +0200] rev 22965

ProofGeneral: Find Theorems search form

haftmann [Mon, 14 May 2007 12:52:56 +0200] rev 22964

reorganized float arithmetic

isabelle