Thu, 28 Jul 2011 10:42:24 +0200 |
simplified definition of vector (also removed Cartesian_Euclidean_Space.from_nat which collides with Countable.from_nat)
|
file | diff | annotate |
Sun, 15 May 2011 17:45:53 +0200 |
simplified/unified method_setup/attribute_setup;
|
file | diff | annotate |
Sun, 28 Nov 2010 15:20:51 +0100 |
gave more standard finite set rules simp and intro attribute
|
file | diff | annotate |
Mon, 13 Sep 2010 11:13:15 +0200 |
renamed lemmas: ext_iff -> fun_eq_iff, set_ext_iff -> set_eq_iff, set_ext -> set_eqI
|
file | diff | annotate |
Tue, 07 Sep 2010 10:05:19 +0200 |
expand_fun_eq -> ext_iff
|
file | diff | annotate |
Mon, 23 Aug 2010 19:35:57 +0200 |
Rewrite the Probability theory.
|
file | diff | annotate |
Fri, 20 Aug 2010 17:46:56 +0200 |
more concise characterization of of_nat operation and class semiring_char_0
|
file | diff | annotate |
Thu, 01 Jul 2010 16:54:44 +0200 |
"prod" and "sum" replace "*" and "+" respectively
|
file | diff | annotate |
Thu, 01 Jul 2010 11:48:42 +0200 |
Add theory for indicator function.
|
file | diff | annotate |
Thu, 01 Jul 2010 09:01:09 +0200 |
Instantiate product type as euclidean space.
|
file | diff | annotate |
Wed, 23 Jun 2010 10:05:13 +0200 |
Make latex happy
|
file | diff | annotate |
Mon, 21 Jun 2010 19:33:51 +0200 |
Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
|
file | diff | annotate |