| Mon, 30 Jun 2014 15:45:21 +0200 |
hoelzl |
import more stuff from the CLT proof; base the lborel measure on interval_measure; remove lebesgue measure
|
file |
diff |
annotate
|
| Wed, 18 Jun 2014 07:31:12 +0200 |
hoelzl |
moved lemmas from the proof of the Central Limit Theorem by Jeremy Avigad and Luke Serafin
|
file |
diff |
annotate
|
| Wed, 07 May 2014 12:25:35 +0200 |
hoelzl |
avoid the Complex constructor, use the more natural Re/Im view; moved csqrt to Complex.
|
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, 19 Mar 2014 17:06:02 +0000 |
paulson |
Some rationalisation of basic lemmas
|
file |
diff |
annotate
|
| Thu, 13 Mar 2014 13:18:13 +0100 |
blanchet |
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
|
file |
diff |
annotate
|
| Thu, 06 Mar 2014 15:40:33 +0100 |
blanchet |
renamed 'fun_rel' to 'rel_fun'
|
file |
diff |
annotate
|
| Wed, 25 Dec 2013 17:39:06 +0100 |
haftmann |
prefer more canonical names for lemmas on min/max
|
file |
diff |
annotate
|
| Tue, 19 Nov 2013 10:05:53 +0100 |
haftmann |
eliminiated neg_numeral in favour of - (numeral _)
|
file |
diff |
annotate
|
| Tue, 05 Nov 2013 21:23:42 +0100 |
hoelzl |
int and nat are conditionally_complete_lattices
|
file |
diff |
annotate
|
| Tue, 05 Nov 2013 09:45:02 +0100 |
hoelzl |
move Lubs from HOL to HOL-Library (replaced by conditionally complete lattices)
|
file |
diff |
annotate
|
| Tue, 05 Nov 2013 09:45:00 +0100 |
hoelzl |
generalize bdd_above/below_uminus to ordered_ab_group_add
|
file |
diff |
annotate
|
| Tue, 05 Nov 2013 09:44:58 +0100 |
hoelzl |
use bdd_above and bdd_below for conditionally complete lattices
|
file |
diff |
annotate
|
| Fri, 01 Nov 2013 18:51:14 +0100 |
haftmann |
more simplification rules on unary and binary minus
|
file |
diff |
annotate
|
| Mon, 16 Sep 2013 15:30:20 +0200 |
kuncar |
use lifting_forget for deregistering numeric types as a quotient type
|
file |
diff |
annotate
|
| Tue, 03 Sep 2013 01:12:40 +0200 |
wenzelm |
tuned proofs -- clarified flow of facts wrt. calculation;
|
file |
diff |
annotate
|
| Sun, 18 Aug 2013 18:49:45 +0200 |
wenzelm |
more symbols;
|
file |
diff |
annotate
|
| Mon, 13 May 2013 13:59:04 +0200 |
kuncar |
better support for domains in Lifting/Transfer = replace Domainp T by the actual invariant in a transferred goal
|
file |
diff |
annotate
|
| Thu, 25 Apr 2013 11:59:21 +0200 |
hoelzl |
revert #916271d52466; add non-topological linear_continuum type class; show linear_continuum_topology is a perfect_space
|
file |
diff |
annotate
|
| Wed, 24 Apr 2013 13:28:30 +0200 |
hoelzl |
spell conditional_ly_-complete lattices correct
|
file |
diff |
annotate
|
| Tue, 26 Mar 2013 15:10:28 +0100 |
wenzelm |
merged
|
file |
diff |
annotate
|
| Tue, 26 Mar 2013 12:20:56 +0100 |
hoelzl |
rename RealDef to Real
|
file |
diff |
annotate
|
| Tue, 26 Mar 2013 12:20:55 +0100 |
hoelzl |
merge RComplete into RealDef
|
file |
diff |
annotate
|
| Wed, 22 Aug 2012 22:55:41 +0200 |
wenzelm |
prefer ML_file over old uses;
|
file |
diff |
annotate
|
| Wed, 12 May 2010 23:54:04 +0200 |
boehmes |
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
|
file |
diff |
annotate
|
| Wed, 10 Feb 2010 14:12:02 +0100 |
haftmann |
moved lemma field_le_epsilon from Real.thy to Fields.thy
|
file |
diff |
annotate
|
| Tue, 09 Feb 2010 16:07:09 +0100 |
haftmann |
simple proofs make life faster and easier
|
file |
diff |
annotate
|
| Fri, 05 Feb 2010 14:33:50 +0100 |
haftmann |
more consistent naming of type classes involving orderings (and lattices) -- c.f. NEWS
|
file |
diff |
annotate
|
| Mon, 05 Oct 2009 17:27:46 +0100 |
paulson |
New lemmas connected with the reals and infinite series
|
file |
diff |
annotate
|
| Mon, 29 Dec 2008 14:08:08 +0100 |
haftmann |
adapted HOL source structure to distribution layout
|
file |
diff |
annotate
|
| Thu, 11 Dec 2008 08:56:02 +0100 |
nipkow |
codegen
|
file |
diff |
annotate
|
| Wed, 10 Dec 2008 10:23:47 +0100 |
nipkow |
moved ContNotDenum into Library
|
file |
diff |
annotate
|
| Wed, 03 Dec 2008 15:58:44 +0100 |
haftmann |
made repository layout more coherent with logical distribution structure; stripped some $Id$s
|
file |
diff |
annotate
| base
|