| 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
|
| Mon, 27 Feb 2017 17:17:26 +0000 |
paulson |
Some new lemmas thanks to Lukas Bulwahn. Also, NEWS.
|
file |
diff |
annotate
|
| Tue, 21 Feb 2017 15:04:01 +0000 |
paulson |
Some new lemmas. Existing lemmas modified to use uniform_limit rather than its expansion
|
file |
diff |
annotate
|
| Tue, 03 Jan 2017 16:48:49 +0000 |
paulson |
A few new lemmas and needed adaptations
|
file |
diff |
annotate
|
| Tue, 22 Nov 2016 16:22:05 +0100 |
nipkow |
added simp rule
|
file |
diff |
annotate
|
| Mon, 17 Oct 2016 17:33:07 +0200 |
nipkow |
setprod -> prod
|
file |
diff |
annotate
|
| Mon, 17 Oct 2016 11:46:22 +0200 |
nipkow |
setsum -> sum
|
file |
diff |
annotate
|
| Mon, 19 Sep 2016 20:06:21 +0200 |
fleury |
left_distrib ~> distrib_right, right_distrib ~> distrib_left
|
file |
diff |
annotate
|
| Sun, 11 Sep 2016 00:14:44 +0200 |
wenzelm |
tuned proofs;
|
file |
diff |
annotate
|
| Thu, 01 Sep 2016 11:53:07 +0200 |
Manuel Eberl |
Some facts about factorial and binomial coefficients
|
file |
diff |
annotate
|
| Thu, 25 Aug 2016 15:50:43 +0200 |
Manuel Eberl |
More analysis lemmas
|
file |
diff |
annotate
|
| Fri, 29 Jul 2016 20:34:07 +0200 |
wenzelm |
more accurate cong del;
|
file |
diff |
annotate
|
| Thu, 28 Jul 2016 20:39:46 +0200 |
wenzelm |
misc tuning and modernization;
|
file |
diff |
annotate
|
| Fri, 22 Jul 2016 11:00:43 +0200 |
wenzelm |
tuned proofs -- avoid unstructured calculation;
|
file |
diff |
annotate
|
| Tue, 12 Jul 2016 22:54:37 +0200 |
wenzelm |
misc tuning and modernization;
|
file |
diff |
annotate
|
| Sat, 09 Jul 2016 13:26:16 +0200 |
haftmann |
more lemmas to emphasize {0::nat..(<)n} as canonical representation of intervals on nat
|
file |
diff |
annotate
|
| Sat, 02 Jul 2016 20:22:25 +0200 |
haftmann |
simplified definitions of combinatorial functions
|
file |
diff |
annotate
|
| Sat, 02 Jul 2016 08:41:05 +0200 |
haftmann |
more theorems
|
file |
diff |
annotate
|
| Mon, 13 Jun 2016 15:23:12 +0200 |
eberlm |
Facts about HK integration, complex powers, Gamma function
|
file |
diff |
annotate
|
| Fri, 27 May 2016 20:23:55 +0200 |
wenzelm |
tuned proofs, to allow unfold_abs_def;
|
file |
diff |
annotate
|
| Wed, 25 May 2016 11:49:40 +0200 |
wenzelm |
isabelle update_cartouches -c -t;
|
file |
diff |
annotate
|
| Fri, 13 May 2016 20:24:10 +0200 |
wenzelm |
eliminated use of empty "assms";
|
file |
diff |
annotate
|
| Mon, 25 Apr 2016 16:09:26 +0200 |
wenzelm |
eliminated old 'def';
|
file |
diff |
annotate
|
| Tue, 12 Apr 2016 11:18:29 +0200 |
immler |
added derivative of scaling in exponential function
|
file |
diff |
annotate
|
| Mon, 11 Apr 2016 16:27:42 +0100 |
paulson |
lots of new theorems for multivariate analysis
|
file |
diff |
annotate
|
| Mon, 21 Mar 2016 11:54:45 +0100 |
hoelzl |
add le_log_of_power and le_log2_of_power by Tobias Nipkow
|
file |
diff |
annotate
|
| Tue, 23 Feb 2016 18:04:31 +0100 |
nipkow |
resolved conflict
|
file |
diff |
annotate
|
| Tue, 23 Feb 2016 16:25:08 +0100 |
nipkow |
more canonical names
|
file |
diff |
annotate
|
| Tue, 23 Feb 2016 15:47:39 +0000 |
paulson |
New and revised material for (multivariate) analysis
|
file |
diff |
annotate
|
| Mon, 22 Feb 2016 14:37:56 +0000 |
paulson |
An assortment of useful lemmas about sums, norm, etc. Also: norm_conv_dist [symmetric] is now a simprule!
|
file |
diff |
annotate
|
| Wed, 17 Feb 2016 21:51:57 +0100 |
haftmann |
generalized some lemmas;
|
file |
diff |
annotate
|
| Wed, 06 Jan 2016 12:18:53 +0100 |
hoelzl |
add the proof of the central limit theorem
|
file |
diff |
annotate
|
| Mon, 04 Jan 2016 17:45:36 +0100 |
eberlm |
Added lots of material on infinite sums, convergence radii, harmonic numbers, Gamma function
|
file |
diff |
annotate
|
| Wed, 30 Dec 2015 14:05:51 +0100 |
wenzelm |
more symbols;
|
file |
diff |
annotate
|
| Wed, 30 Dec 2015 11:21:54 +0100 |
wenzelm |
more symbols;
|
file |
diff |
annotate
|
| Tue, 29 Dec 2015 23:04:53 +0100 |
wenzelm |
more symbols;
|
file |
diff |
annotate
|
| Mon, 28 Dec 2015 01:26:34 +0100 |
wenzelm |
prefer symbols for "abs";
|
file |
diff |
annotate
|
| Sun, 27 Dec 2015 21:46:36 +0100 |
wenzelm |
prefer symbols for "floor", "ceiling";
|
file |
diff |
annotate
|
| Mon, 21 Dec 2015 14:44:44 +0100 |
hoelzl |
Transcendental: use [simp]-canonical form - (pi/2)
|
file |
diff |
annotate
|
| Wed, 09 Dec 2015 17:35:22 +0000 |
paulson |
sorted out eventually_mono
|
file |
diff |
annotate
|
| Mon, 07 Dec 2015 10:38:04 +0100 |
wenzelm |
isabelle update_cartouches -c -t;
|
file |
diff |
annotate
|
| Tue, 01 Dec 2015 14:09:10 +0000 |
paulson |
Removal of redundant lemmas (diff_less_iff, diff_le_iff) and of the abbreviation Exp. Addition of some new material.
|
file |
diff |
annotate
|
| Mon, 23 Nov 2015 16:57:54 +0000 |
paulson |
New material about paths, winding numbers, etc. Added lemmas to divide_const_simps. Misc tuning.
|
file |
diff |
annotate
|
| Tue, 17 Nov 2015 12:32:08 +0000 |
paulson |
Removed some legacy theorems; minor adjustments to simplification rules; new material on homotopic paths
|
file |
diff |
annotate
|
| Fri, 13 Nov 2015 12:27:13 +0000 |
paulson |
Tweaks for "real": Removal of [iff] status for some lemmas, adding [simp] for others. Plus fixes.
|
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
|
| Mon, 02 Nov 2015 16:17:09 +0100 |
eberlm |
Added binomial identities to CONTRIBUTORS; small lemmas on of_int/pochhammer
|
file |
diff |
annotate
|
| Mon, 02 Nov 2015 11:56:28 +0100 |
eberlm |
Rounding function, uniform limits, cotangent, binomial identities
|
file |
diff |
annotate
|
| Thu, 29 Oct 2015 15:40:52 +0100 |
eberlm |
added many small lemmas about setsum/setprod/powr/...
|
file |
diff |
annotate
|
| Mon, 26 Oct 2015 23:41:27 +0000 |
paulson |
new lemmas about topology, etc., for Cauchy integral formula
|
file |
diff |
annotate
|
| Wed, 30 Sep 2015 16:36:42 +0100 |
paulson |
real_of_nat_Suc is now a simprule
|
file |
diff |
annotate
|
| Tue, 01 Sep 2015 22:32:58 +0200 |
wenzelm |
eliminated \<Colon>;
|
file |
diff |
annotate
|
| Mon, 31 Aug 2015 21:28:08 +0200 |
wenzelm |
prefer symbols;
|
file |
diff |
annotate
|
| Thu, 06 Aug 2015 23:56:48 +0200 |
haftmann |
slight cleanup of lemmas
|
file |
diff |
annotate
|
| Mon, 20 Jul 2015 23:12:50 +0100 |
paulson |
new material for multivariate analysis, etc.
|
file |
diff |
annotate
|
| Sat, 18 Jul 2015 22:58:50 +0200 |
wenzelm |
isabelle update_cartouches;
|
file |
diff |
annotate
|
| Tue, 14 Jul 2015 13:48:03 +0200 |
hoelzl |
generalized filtermap_homeomorph to filtermap_fun_inverse; add eventually_at_top/bot_not_equal
|
file |
diff |
annotate
|
| Wed, 08 Jul 2015 14:01:41 +0200 |
haftmann |
avoid explicit definition of the relation of associated elements in a ring -- prefer explicit normalization instead
|
file |
diff |
annotate
|
| Mon, 25 May 2015 22:11:43 +0200 |
wenzelm |
merged, resolving conflicts in Admin/isatest/settings/afp-poly and src/HOL/Tools/Nitpick/nitpick_model.ML;
|
file |
diff |
annotate
|
| Sun, 03 May 2015 16:45:07 +0200 |
wenzelm |
tuned;
|
file |
diff |
annotate
|
| Thu, 07 May 2015 15:34:28 +0200 |
hoelzl |
generalized tends over powr; added DERIV rule for powr
|
file |
diff |
annotate
|
| Thu, 30 Apr 2015 15:28:01 +0100 |
paulson |
tidying some messy proofs
|
file |
diff |
annotate
|
| Wed, 29 Apr 2015 14:04:22 +0100 |
paulson |
Tidying. Improved simplification for numerals, esp in exponents.
|
file |
diff |
annotate
|
| Tue, 28 Apr 2015 16:23:38 +0100 |
paulson |
New material about complex transcendental functions (especially Ln, Arg) and polynomials
|
file |
diff |
annotate
|
| Tue, 21 Apr 2015 17:19:00 +0100 |
paulson |
New material, mostly about limits. Consolidation.
|
file |
diff |
annotate
|
| Sun, 12 Apr 2015 11:33:19 +0200 |
hoelzl |
move filters to their own theory
|
file |
diff |
annotate
|
| Sun, 12 Apr 2015 16:04:53 +0200 |
hoelzl |
fix latex in Transcendental
|
file |
diff |
annotate
|
| Sat, 11 Apr 2015 22:18:33 +0100 |
paulson |
Complex roots of unity. Better definition of ln for complex numbers. Used [code del] to stop code generation for powr.
|
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
|
| Wed, 01 Apr 2015 14:08:17 +0100 |
paulson |
arcsin and arccos lemmas
|
file |
diff |
annotate
|
| Tue, 31 Mar 2015 21:54:32 +0200 |
haftmann |
given up separate type classes demanding `inverse 0 = 0`
|
file |
diff |
annotate
|
| Tue, 31 Mar 2015 16:48:48 +0100 |
paulson |
rationalised and generalised some theorems concerning abs and x^2.
|
file |
diff |
annotate
|
| Tue, 31 Mar 2015 15:00:03 +0100 |
paulson |
New material and binomial fix
|
file |
diff |
annotate
|
| Thu, 19 Mar 2015 14:24:51 +0000 |
paulson |
New material for complex sin, cos, tan, Ln, also some reorganisation
|
file |
diff |
annotate
|
| Wed, 18 Mar 2015 17:23:22 +0000 |
paulson |
new HOL Light material about exp, sin, cos
|
file |
diff |
annotate
|
| Wed, 18 Mar 2015 14:13:27 +0000 |
paulson |
Lots of new material on complex-valued functions. Modified simplification of (x/n)^k
|
file |
diff |
annotate
|
| Tue, 17 Mar 2015 12:23:56 +0000 |
paulson |
Merge
|
file |
diff |
annotate
|
| Mon, 16 Mar 2015 15:30:00 +0000 |
paulson |
The factorial function, "fact", now has type "nat => 'a"
|
file |
diff |
annotate
|
| Fri, 13 Mar 2015 12:44:16 +0100 |
wenzelm |
removed junk;
|
file |
diff |
annotate
|
| Tue, 10 Mar 2015 16:12:35 +0000 |
paulson |
renaming HOL/Fact.thy -> Binomial.thy
|
file |
diff |
annotate
|
| Mon, 09 Mar 2015 16:28:19 +0000 |
paulson |
sin, cos generalised from type real to any "'a::{real_normed_field,banach}", including complex
|
file |
diff |
annotate
|
| Sat, 07 Mar 2015 21:32:31 +0100 |
wenzelm |
clarified Drule.gen_all: observe context more carefully;
|
file |
diff |
annotate
|
| Thu, 05 Mar 2015 17:30:29 +0000 |
paulson |
The function frac. Various lemmas about limits, series, the exp function, etc.
|
file |
diff |
annotate
|
| Wed, 04 Mar 2015 23:31:04 +0100 |
nipkow |
Removed the obsolete functions "natfloor" and "natceiling"
|
file |
diff |
annotate
|
| Wed, 12 Nov 2014 17:36:36 +0100 |
immler |
added lemmas: convert between powr and log in comparisons, pull log out of addition/subtraction
|
file |
diff |
annotate
|
| Wed, 12 Nov 2014 17:36:25 +0100 |
immler |
code equation for powr
|
file |
diff |
annotate
|
| Sun, 02 Nov 2014 18:21:45 +0100 |
wenzelm |
modernized header uniformly as section;
|
file |
diff |
annotate
|
| Thu, 30 Oct 2014 21:02:01 +0100 |
haftmann |
more simp rules concerning dvd and even/odd
|
file |
diff |
annotate
|
| Tue, 21 Oct 2014 21:10:44 +0200 |
haftmann |
turn even into an abbreviation
|
file |
diff |
annotate
|
| Mon, 20 Oct 2014 18:33:14 +0200 |
hoelzl |
add tendsto_const and tendsto_ident_at as simp and intro rules
|
file |
diff |
annotate
|
| Mon, 20 Oct 2014 07:45:58 +0200 |
haftmann |
augmented and tuned facts on even/odd and division
|
file |
diff |
annotate
|
| Sun, 19 Oct 2014 18:05:26 +0200 |
haftmann |
prefer generic elimination rules for even/odd over specialized unfold rules for nat
|
file |
diff |
annotate
|
| Mon, 13 Oct 2014 18:55:05 +0200 |
immler |
relaxed class constraints for exp
|
file |
diff |
annotate
|