| Sun, 21 Oct 2018 09:39:09 +0200 |
nipkow |
uniform naming of strong congruence rules
|
file |
diff |
annotate
|
| Sun, 15 Apr 2018 13:57:00 +0100 |
paulson |
various new results on measures, integrals, etc., and some simplified proofs
|
file |
diff |
annotate
|
| Mon, 17 Oct 2016 11:46:22 +0200 |
nipkow |
setsum -> sum
|
file |
diff |
annotate
|
| Fri, 30 Sep 2016 16:08:38 +0200 |
hoelzl |
HOL-Probability: more about probability, prepare for Markov processes in the AFP
|
file |
diff |
annotate
|
| Fri, 16 Sep 2016 13:56:51 +0200 |
hoelzl |
move Henstock-Kurzweil integration after Lebesgue_Measure; replace content by abbreviation measure lborel
|
file |
diff |
annotate
|
| Fri, 05 Aug 2016 18:34:57 +0200 |
hoelzl |
move measure theory from HOL-Probability to HOL-Multivariate_Analysis
|
file |
diff |
annotate
|
| Fri, 29 Jul 2016 20:34:07 +0200 |
wenzelm |
more accurate cong del;
|
file |
diff |
annotate
|
| Mon, 25 Apr 2016 16:09:26 +0200 |
wenzelm |
eliminated old 'def';
|
file |
diff |
annotate
|
| Thu, 14 Apr 2016 15:48:11 +0200 |
hoelzl |
Probability: move emeasure and nn_integral from ereal to ennreal
|
file |
diff |
annotate
|
| Tue, 23 Feb 2016 16:25:08 +0100 |
nipkow |
more canonical names
|
file |
diff |
annotate
|
| Mon, 07 Dec 2015 20:19:59 +0100 |
wenzelm |
isabelle update_cartouches -c -t;
|
file |
diff |
annotate
|
| Tue, 10 Nov 2015 14:18:41 +0000 |
paulson |
Coercion "real" now has type nat => real only and is no longer overloaded. Type class "real_of" is gone. Many duplicate theorems removed.
|
file |
diff |
annotate
|
| Sun, 13 Sep 2015 22:56:52 +0200 |
wenzelm |
tuned proofs -- less legacy;
|
file |
diff |
annotate
|
| Thu, 25 Jun 2015 23:33:47 +0200 |
wenzelm |
tuned proofs;
|
file |
diff |
annotate
|
| Sat, 11 Apr 2015 11:56:40 +0100 |
paulson |
Overloading of ln and powr, but "approximation" no longer works for powr. Code generation also fails due to type ambiguity in scala.
|
file |
diff |
annotate
|
| Sun, 02 Nov 2014 17:06:05 +0100 |
wenzelm |
modernized header;
|
file |
diff |
annotate
|
| Sat, 28 Jun 2014 09:16:42 +0200 |
haftmann |
fact consolidation
|
file |
diff |
annotate
|
| Fri, 13 Jun 2014 14:08:20 +0200 |
hoelzl |
properties of normal distributed random variables (by Sudeep Kanav)
|
file |
diff |
annotate
|
| Thu, 12 Jun 2014 15:47:36 +0200 |
hoelzl |
properties of Erlang and exponentially distributed random variables (by Sudeep Kanav)
|
file |
diff |
annotate
|
| Tue, 03 Jun 2014 16:22:01 +0200 |
hoelzl |
use 0 as integral-value for non-integrable functions, simplify a couple of rewrite rules
|
file |
diff |
annotate
|
| Mon, 19 May 2014 14:26:58 +0200 |
hoelzl |
renamed positive_integral to nn_integral
|
file |
diff |
annotate
|
| Mon, 19 May 2014 13:44:13 +0200 |
hoelzl |
fixed document generation for HOL-Probability
|
file |
diff |
annotate
|
| Mon, 19 May 2014 12:04:45 +0200 |
hoelzl |
introduce Bochner integral: generalizes Lebesgue integral from real-valued function to functions on real-normed vector spaces
|
file |
diff |
annotate
|
| Mon, 14 Apr 2014 13:08:17 +0200 |
hoelzl |
added divide_nonneg_nonneg and co; made it a simp rule
|
file |
diff |
annotate
|
| Sat, 12 Apr 2014 17:26:27 +0200 |
nipkow |
made mult_pos_pos a simp rule
|
file |
diff |
annotate
|
| Fri, 11 Apr 2014 22:53:33 +0200 |
nipkow |
made divide_pos_pos a simp rule
|
file |
diff |
annotate
|
| Fri, 11 Apr 2014 13:36:57 +0200 |
nipkow |
made mult_nonneg_nonneg a simp rule
|
file |
diff |
annotate
|
| Wed, 09 Apr 2014 09:37:47 +0200 |
hoelzl |
revert c1bbd3e22226, a14831ac3023, and 36489d77c484: divide_minus_left/right are again simp rules
|
file |
diff |
annotate
|
| Thu, 03 Apr 2014 23:51:52 +0100 |
paulson |
removing simprule status for divide_minus_left and divide_minus_right
|
file |
diff |
annotate
|
| Sat, 15 Mar 2014 08:31:33 +0100 |
haftmann |
more complete set of lemmas wrt. image and composition
|
file |
diff |
annotate
|