| Thu, 08 Jul 2021 08:44:18 +0200 |
desharna |
merged
|
file |
diff |
annotate
|
| Thu, 08 Jul 2021 08:42:36 +0200 |
desharna |
added opaque_combs and renamed hide_lams to opaque_lifting
|
file |
diff |
annotate
|
| Sun, 04 Jul 2021 18:35:57 +0100 |
paulson |
Imported lots of material from Stirling_Formula/Gamma_Asymptotics
|
file |
diff |
annotate
|
| Sun, 09 May 2021 05:48:50 +0000 |
haftmann |
more elementary swap
|
file |
diff |
annotate
|
| Wed, 07 Apr 2021 12:28:19 +0000 |
haftmann |
simplified definition
|
file |
diff |
annotate
|
| Wed, 11 Nov 2020 14:27:17 +0000 |
paulson |
mult_le_cancel_iff1, mult_le_cancel_iff2, mult_less_iff1 generalised from the real_ versions
|
file |
diff |
annotate
|
| Sun, 11 Oct 2020 14:56:03 +0100 |
paulson |
tidying and removal of legacy name
|
file |
diff |
annotate
|
| Tue, 31 Mar 2020 15:51:15 +0200 |
nipkow |
cleaned proofs
|
file |
diff |
annotate
|
| Mon, 02 Dec 2019 14:22:03 +0100 |
Manuel Eberl |
Flattened dependency tree of HOL-Analysis
|
file |
diff |
annotate
|
| Sat, 30 Nov 2019 13:47:33 +0100 |
Manuel Eberl |
Split off new HOL-Complex_Analysis session from HOL-Analysis
|
file |
diff |
annotate
|
| Thu, 28 Nov 2019 23:06:22 +0100 |
nipkow |
tuned
|
file |
diff |
annotate
|
| Wed, 09 Oct 2019 14:51:54 +0000 |
haftmann |
dedicated fact collections for algebraic simplification rules potentially splitting goals
|
file |
diff |
annotate
|
| Tue, 08 Oct 2019 10:26:40 +0000 |
haftmann |
formally augmented corresponding rules for field_simps
|
file |
diff |
annotate
|
| Thu, 19 Sep 2019 12:36:15 +0100 |
paulson |
A few more simple results
|
file |
diff |
annotate
|
| Mon, 16 Sep 2019 17:03:13 +0100 |
paulson |
A little-known material, and some tidying up
|
file |
diff |
annotate
|
| Fri, 16 Aug 2019 12:53:36 +0100 |
paulson |
new material on eqiintegrable functions, etc.
|
file |
diff |
annotate
|
| Thu, 15 Aug 2019 16:11:56 +0100 |
paulson |
new material; rotated premises of Lim_transform_eventually
|
file |
diff |
annotate
|
| Thu, 18 Jul 2019 15:40:15 +0100 |
paulson |
More analysis / measure theory material
|
file |
diff |
annotate
|
| Thu, 18 Jul 2019 14:08:28 +0100 |
paulson |
more new material about analysis
|
file |
diff |
annotate
|
| Wed, 17 Jul 2019 14:02:42 +0100 |
paulson |
a few new lemmas and a bit of tidying
|
file |
diff |
annotate
|
| Fri, 12 Apr 2019 22:52:00 +0200 |
wenzelm |
avoid Isabelle symbols in URL;
|
file |
diff |
annotate
|
| Fri, 12 Apr 2019 22:24:57 +0200 |
wenzelm |
formal URLs;
|
file |
diff |
annotate
|
| Fri, 12 Apr 2019 22:09:25 +0200 |
wenzelm |
modernized tags: default scope excludes proof;
|
file |
diff |
annotate
|
| Tue, 19 Mar 2019 16:14:51 +0000 |
paulson |
new material about topology, etc.; also fixes for yesterday's
|
file |
diff |
annotate
|
| Fri, 25 Jan 2019 14:59:40 +0100 |
nipkow |
tuned
|
file |
diff |
annotate
|
| Tue, 22 Jan 2019 21:13:23 +0000 |
Angeliki KoutsoukouArgyraki |
redid tagging for 3 theories i.e. Determinants, Change_of_Vars, Finite_Cartesian_Product
|
file |
diff |
annotate
|
| Thu, 17 Jan 2019 16:38:00 -0500 |
immler |
subsection is always %important
|
file |
diff |
annotate
|
| Thu, 17 Jan 2019 16:08:41 +0000 |
Angeliki KoutsoukouArgyraki |
merge
|
file |
diff |
annotate
|
| Wed, 16 Jan 2019 21:27:33 +0000 |
Angeliki KoutsoukouArgyraki |
updated tagging for 9 theories: Cross3, Determinants, Tagged_Division, Change_of_Vars, Extended_Real_Limits, Fashoda, Finite_Cartesian_Product, Function_Topology, Finite_Product_Measure
|
file |
diff |
annotate
|
| Wed, 16 Jan 2019 18:14:02 -0500 |
immler |
Reorg, in particular Determinants as well as some linear algebra from Starlike and Change_Of_Vars
|
file |
diff |
annotate
|