| Wed, 06 Jun 2007 20:49:04 +0200 | huffman | add axclass semiring_char_0 for types where of_nat is injective | file | diff | annotate |
| Wed, 30 May 2007 02:41:26 +0200 | huffman | simplify names of locale interpretations | file | diff | annotate |
| Tue, 29 May 2007 18:19:56 +0200 | huffman | interpretation bounded_linear_divide | file | diff | annotate |
| Mon, 28 May 2007 04:22:44 +0200 | huffman | interpretations additive_scaleR_left, additive_scaleR_right | file | diff | annotate |
| 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 | file | diff | annotate |
| Mon, 14 May 2007 20:14:31 +0200 | huffman | generalized sgn function to work on any real normed vector space | file | diff | annotate |
| Sat, 12 May 2007 18:16:30 +0200 | huffman | add lemma additive.setsum | file | diff | annotate |