| 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
|
| Tue, 20 May 2014 19:24:39 +0200 |
hoelzl |
add various lemmas
|
file |
diff |
annotate
|
| Tue, 13 May 2014 11:35:47 +0200 |
hoelzl |
clean up Lebesgue integration
|
file |
diff |
annotate
|
| Thu, 10 Apr 2014 17:48:18 +0200 |
kuncar |
setup for Transfer and Lifting from BNF; tuned thm names
|
file |
diff |
annotate
|
| Thu, 10 Apr 2014 17:48:14 +0200 |
kuncar |
left_total and left_unique rules are now transfer rules (cleaner solution, reflexvity_rule attribute not needed anymore)
|
file |
diff |
annotate
|
| Wed, 02 Apr 2014 18:35:07 +0200 |
hoelzl |
extend continuous_intros; remove continuous_on_intros and isCont_intros
|
file |
diff |
annotate
|
| Mon, 31 Mar 2014 12:16:37 +0200 |
hoelzl |
add connected_local_const
|
file |
diff |
annotate
|
| Wed, 26 Mar 2014 14:00:37 +0000 |
paulson |
Some useful lemmas
|
file |
diff |
annotate
|
| Thu, 20 Mar 2014 21:07:57 +0100 |
wenzelm |
enforce subgoal boundaries via SUBGOAL/SUBGOAL_CASES -- clean tactical failure if out-of-range;
|
file |
diff |
annotate
|
| Sun, 16 Mar 2014 18:09:04 +0100 |
haftmann |
normalising simp rules for compound operators
|
file |
diff |
annotate
|
| Mon, 10 Mar 2014 20:04:40 +0100 |
hoelzl |
introduced antimono; incseq, decseq are now abbreviations for mono and antimono; renamed Library/Continuity to Library/Order_Continuity; removed up_cont; renamed down_cont to down_continuity and generalized to complete_lattices
|
file |
diff |
annotate
|
| Thu, 06 Mar 2014 15:40:33 +0100 |
blanchet |
renamed 'fun_rel' to 'rel_fun'
|
file |
diff |
annotate
|
| Thu, 06 Mar 2014 15:14:09 +0100 |
blanchet |
renamed 'filter_rel' to 'rel_filter'
|
file |
diff |
annotate
|
| Thu, 06 Mar 2014 14:57:14 +0100 |
blanchet |
renamed 'set_rel' to 'rel_set'
|
file |
diff |
annotate
|
| Thu, 27 Feb 2014 16:07:21 +0000 |
paulson |
A bit of tidying up
|
file |
diff |
annotate
|