| Tue, 26 Oct 2021 14:43:59 +0000 |
haftmann |
more generic bit/word lemmas for distribution
|
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
|
| Wed, 23 Dec 2020 16:25:52 +0000 |
paulson |
default simprule for geometric series
|
file |
diff |
annotate
|
| Thu, 27 Aug 2020 15:23:48 +0100 |
paulson |
but not the [cong] rule
|
file |
diff |
annotate
|
| Thu, 27 Aug 2020 12:14:46 +0100 |
paulson |
tidying up some theorem statements
|
file |
diff |
annotate
|
| Wed, 26 Aug 2020 15:59:21 +0100 |
paulson |
tiny tidy-up of proofs
|
file |
diff |
annotate
|
| Fri, 19 Jun 2020 09:46:47 +0000 |
haftmann |
prefer single name
|
file |
diff |
annotate
|
| Thu, 04 Jun 2020 15:30:22 +0000 |
haftmann |
more simp rules
|
file |
diff |
annotate
|
| Wed, 13 May 2020 12:55:33 +0200 |
Manuel Eberl |
new constant power_int in HOL
|
file |
diff |
annotate
|
| Sun, 22 Mar 2020 17:21:16 +0000 |
paulson |
tidying up some horrible proofs
|
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
|
| Wed, 18 Sep 2019 14:41:37 +0100 |
paulson |
imported new material mostly due to Sébastien Gouëzel
|
file |
diff |
annotate
|
| Tue, 17 Sep 2019 16:21:31 +0100 |
paulson |
A couple of new theorems, stolen from AFP entries
|
file |
diff |
annotate
|
| Thu, 15 Aug 2019 16:11:56 +0100 |
paulson |
new material; rotated premises of Lim_transform_eventually
|
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, 14 Jun 2019 08:34:28 +0000 |
haftmann |
moved some theorems into HOL main corpus
|
file |
diff |
annotate
|
| Wed, 15 May 2019 12:47:15 +0100 |
paulson |
Generalisations involving numerals; comparisons should now work for ennreal
|
file |
diff |
annotate
|
| Wed, 10 Apr 2019 21:29:32 +0100 |
paulson |
Fixing the main Homology theory; also moving a lot of sum/prod lemmas into their generic context
|
file |
diff |
annotate
|
| Wed, 10 Apr 2019 13:34:55 +0100 |
paulson |
The last big tranche of Homology material: invariance of domain; renamings to use generic sum/prod lemmas from their locale
|
file |
diff |
annotate
|
| Mon, 14 Jan 2019 14:46:12 +0100 |
nipkow |
uniform naming
|
file |
diff |
annotate
|
| Fri, 04 Jan 2019 23:22:53 +0100 |
wenzelm |
isabelle update -u control_cartouches;
|
file |
diff |
annotate
|
| Thu, 08 Nov 2018 22:29:09 +0100 |
wenzelm |
isabelle update_cartouches -t;
|
file |
diff |
annotate
|
| Sun, 21 Oct 2018 09:39:09 +0200 |
nipkow |
uniform naming of strong congruence rules
|
file |
diff |
annotate
|
| Thu, 20 Sep 2018 18:20:02 +0100 |
paulson |
removal of more redundancies, and fixes
|
file |
diff |
annotate
|
| Thu, 20 Sep 2018 14:17:58 +0100 |
paulson |
elimination of near duplication involving Rolle's theorem and the MVT
|
file |
diff |
annotate
|
| Fri, 17 Aug 2018 11:26:35 +0000 |
haftmann |
proper code abbreviation for power on real
|
file |
diff |
annotate
|
| Mon, 16 Jul 2018 15:24:06 +0200 |
Manuel Eberl |
Made simproc for sqrt/root of numeral more robust
|
file |
diff |
annotate
|
| Sun, 15 Jul 2018 21:58:50 +0100 |
paulson |
de-applying and meta-quantifying
|
file |
diff |
annotate
|
| Sun, 15 Jul 2018 16:05:38 +0100 |
paulson |
fixes and more de-applying
|
file |
diff |
annotate
|
| Sun, 15 Jul 2018 13:15:31 +0100 |
paulson |
more de-applying and a fix
|
file |
diff |
annotate
|
| Wed, 11 Jul 2018 15:36:12 +0100 |
paulson |
more de-applying
|
file |
diff |
annotate
|
| Tue, 10 Jul 2018 23:18:08 +0100 |
paulson |
de-applying, etc.
|
file |
diff |
annotate
|
| Sun, 08 Jul 2018 11:00:20 +0100 |
paulson |
De-applying
|
file |
diff |
annotate
|
| Sat, 07 Jul 2018 15:07:37 +0100 |
paulson |
de-applying, etc.
|
file |
diff |
annotate
|
| Thu, 05 Jul 2018 23:37:00 +0100 |
paulson |
de-applying
|
file |
diff |
annotate
|
| Thu, 28 Jun 2018 14:13:57 +0100 |
paulson |
Generalising and renaming some basic results
|
file |
diff |
annotate
|
| Tue, 26 Jun 2018 14:51:18 +0100 |
paulson |
Rationalisation of complex transcendentals, esp the Arg function
|
file |
diff |
annotate
|
| Sun, 06 May 2018 18:20:25 +0000 |
haftmann |
removed some lemma duplicates
|
file |
diff |
annotate
|
| Thu, 03 May 2018 22:34:49 +0100 |
paulson |
Some tidying up (mostly regarding summations from 0)
|
file |
diff |
annotate
|
| Mon, 26 Feb 2018 07:34:05 +0100 |
immler |
moved Lipschitz continuity from AFP/Ordinary_Differential_Equations and AFP/Gromov_Hyperbolicity; moved lemmas from AFP/Gromov_Hyperbolicity/Library_Complements
|
file |
diff |
annotate
|
| Thu, 22 Feb 2018 15:17:25 +0100 |
immler |
moved theorems from AFP/Affine_Arithmetic and AFP/Ordinary_Differential_Equations
|
file |
diff |
annotate
|
| Wed, 07 Feb 2018 18:08:12 +0100 |
eberlm |
Added hyperbolic functions
|
file |
diff |
annotate
|
| Mon, 05 Feb 2018 08:30:19 +0100 |
immler |
added lemmas, avoid 'float_of 0'
|
file |
diff |
annotate
|
| Tue, 16 Jan 2018 09:30:00 +0100 |
wenzelm |
standardized towards new-style formal comments: isabelle update_comments;
|
file |
diff |
annotate
|
| Wed, 10 Jan 2018 15:25:09 +0100 |
nipkow |
ran isabelle update_op on all sources
|
file |
diff |
annotate
|
| Fri, 22 Dec 2017 21:00:07 +0000 |
paulson |
new/improved theories involving convergence; better pretty-printing for bounded quantifiers and sum/product
|
file |
diff |
annotate
|
| Sun, 26 Nov 2017 21:08:32 +0100 |
wenzelm |
more symbols;
|
file |
diff |
annotate
|
| Tue, 10 Oct 2017 17:15:37 +0100 |
paulson |
Divided Topology_Euclidean_Space in two, creating new theory Connected. Also deleted some duplicate / variant theorems
|
file |
diff |
annotate
|
| Sun, 27 Aug 2017 13:02:13 +0200 |
nipkow |
tuned
|
file |
diff |
annotate
|
| Sat, 26 Aug 2017 16:47:25 +0200 |
nipkow |
reorganized and added log-related lemmas
|
file |
diff |
annotate
|
| Sat, 26 Aug 2017 09:10:42 +0200 |
nipkow |
tuned proofs
|
file |
diff |
annotate
|
| Fri, 25 Aug 2017 23:09:56 +0200 |
nipkow |
reorganization of tree lemmas; new lemmas
|
file |
diff |
annotate
|
| Tue, 22 Aug 2017 21:36:48 +0200 |
Manuel Eberl |
Lemmas about analysis and permutations
|
file |
diff |
annotate
|
| Sat, 15 Jul 2017 14:54:13 +0100 |
eberlm |
Simprocs for roots of numerals
|
file |
diff |
annotate
|
| Tue, 02 May 2017 14:34:06 +0100 |
paulson |
Simplification of some proofs. Also key lemmas using !! rather than ! in premises
|
file |
diff |
annotate
|
| Wed, 26 Apr 2017 15:53:35 +0100 |
paulson |
Further new material. The simprule status of some exp and ln identities was reverted.
|
file |
diff |
annotate
|
| Tue, 25 Apr 2017 16:39:54 +0100 |
paulson |
New material from PNT proof, as well as more default [simp] declarations. Also removed duplicate theorems about geometric series
|
file |
diff |
annotate
|
| Sat, 22 Apr 2017 22:01:35 +0200 |
wenzelm |
theories "GCD" and "Binomial" are already included in "Main": this avoids improper imports in applications;
|
file |
diff |
annotate
|
| Fri, 10 Mar 2017 23:16:40 +0100 |
immler |
modernized construction of type bcontfun; base explicit theorems on Uniform_Limit.thy; added some lemmas
|
file |
diff |
annotate
|
| Sun, 05 Mar 2017 10:57:51 +0100 |
nipkow |
added numeral_powr_numeral
|
file |
diff |
annotate
|