#
a1f8bb2d |
|
18-Sep-2019 |
paulson <lp15@cam.ac.uk> |
imported new material mostly due to Sébastien Gouëzel
|
#
35216754 |
|
10-Apr-2019 |
paulson <lp15@cam.ac.uk> |
Fixing the main Homology theory; also moving a lot of sum/prod lemmas into their generic context
|
#
48a391b7 |
|
10-Apr-2019 |
paulson <lp15@cam.ac.uk> |
The last big tranche of Homology material: invariance of domain; renamings to use generic sum/prod lemmas from their locale
|
#
a4bab154 |
|
04-Jan-2019 |
wenzelm <none@none> |
isabelle update -u control_cartouches;
|
#
6243d81c |
|
30-Aug-2018 |
Manuel Eberl <eberlm@in.tum.de> |
Some basic materials on filters and topology --HG-- extra : rebase_source : af17e025be84916013ccf7c6ca0f669ec047aa54
|
#
0fdd6bca |
|
03-Aug-2018 |
eberlm <eberlm@in.tum.de> |
Small lemmas about analysis --HG-- extra : rebase_source : d857a4b442d3d409faf82354bcbb2e39b5445956
|
#
3f439188 |
|
05-Jul-2018 |
paulson <lp15@cam.ac.uk> |
de-applying
|
#
a0960b42 |
|
28-Jun-2018 |
paulson <lp15@cam.ac.uk> |
Generalising and renaming some basic results
|
#
102fb118 |
|
26-Jun-2018 |
paulson <lp15@cam.ac.uk> |
Rationalisation of complex transcendentals, esp the Arg function
|
#
9d151cd5 |
|
09-May-2018 |
paulson <lp15@cam.ac.uk> |
more infinite product theorems
|
#
27050edb |
|
01-May-2018 |
paulson <lp15@cam.ac.uk> |
type class generalisations; some work on infinite products
|
#
fea6a4cc |
|
22-Dec-2017 |
paulson <lp15@cam.ac.uk> |
new/improved theories involving convergence; better pretty-printing for bounded quantifiers and sum/product
|
#
56bf032a |
|
12-Dec-2017 |
Manuel Eberl <eberlm@in.tum.de> |
Moved analysis material from AFP
|
#
d56872f7 |
|
19-Aug-2017 |
Manuel Eberl <eberlm@in.tum.de> |
Various lemmas for HOL-Analysis
|
#
c2d49d41 |
|
17-Aug-2017 |
eberlm <eberlm@in.tum.de> |
Replaced subseq with strict_mono
|
#
3f3e576c |
|
02-May-2017 |
paulson <lp15@cam.ac.uk> |
Simplification of some proofs. Also key lemmas using !! rather than ! in premises
|
#
351cc2e6 |
|
17-Oct-2016 |
nipkow <none@none> |
setsum -> sum
|
#
dc1c0020 |
|
28-Sep-2016 |
paulson <lp15@cam.ac.uk> |
new material connected with HOL Light measure theory, plus more rationalisation
|
#
9b9c2176 |
|
12-Aug-2016 |
wenzelm <none@none> |
more symbols;
|
#
2dc408f1 |
|
26-Jul-2016 |
wenzelm <none@none> |
misc tuning and modernization;
|
#
0f0a91d1 |
|
02-Jul-2016 |
haftmann <none@none> |
more theorems
|
#
ddacf0c0 |
|
25-May-2016 |
wenzelm <none@none> |
isabelle update_cartouches -c -t;
|
#
a2bc0021 |
|
25-Apr-2016 |
wenzelm <none@none> |
eliminated old 'def'; tuned comments;
|
#
fd7948b3 |
|
23-Feb-2016 |
paulson <lp15@cam.ac.uk> |
New and revised material for (multivariate) analysis
|
#
259fcfd2 |
|
22-Feb-2016 |
paulson <lp15@cam.ac.uk> |
An assortment of useful lemmas about sums, norm, etc. Also: norm_conv_dist [symmetric] is now a simprule!
|
#
3042fd7a |
|
12-Feb-2016 |
hoelzl <none@none> |
moved more proofs to ordered_comm_monoid_add; introduced strict_ordered_ab_semigroup/comm_monoid_add --HG-- extra : rebase_source : 8674c79985a670cee921b8193965bb0767549a5c
|
#
cef8f2ad |
|
10-Feb-2016 |
hoelzl <none@none> |
Rename ordered_comm_monoid_add to ordered_cancel_comm_monoid_add. Introduce ordreed_comm_monoid_add, canonically_ordered_comm_monoid and dioid. Setup nat, entat and ennreal as dioids. --HG-- extra : rebase_source : 54bd3e5fcde04ef38241be91231c48d078b850f2
|
#
30fd351a |
|
08-Feb-2016 |
hoelzl <none@none> |
add type class for topological monoids --HG-- extra : rebase_source : bedca3d32972c3f447e37ac5aac3de5ac763b94b
|
#
8214bd46 |
|
22-Jan-2016 |
paulson <lp15@cam.ac.uk> |
Reorganised a huge proof
|
#
8b08bf14 |
|
07-Jan-2016 |
paulson <none@none> |
revisions to limits and derivatives, plus new lemmas
|
#
e68c51f7 |
|
04-Jan-2016 |
eberlm <none@none> |
Added lots of material on infinite sums, convergence radii, harmonic numbers, Gamma function
|
#
6d3e0a15 |
|
29-Dec-2015 |
wenzelm <none@none> |
more symbols;
|
#
0df376fc |
|
07-Dec-2015 |
wenzelm <none@none> |
isabelle update_cartouches -c -t;
|
#
3f106d8a |
|
10-Nov-2015 |
paulson <lp15@cam.ac.uk> |
Coercion "real" now has type nat => real only and is no longer overloaded. Type class "real_of" is gone. Many duplicate theorems removed.
|
#
dd88f1ec |
|
02-Nov-2015 |
eberlm <none@none> |
Rounding function, uniform limits, cotangent, binomial identities
|
#
6ee65982 |
|
06-Aug-2015 |
haftmann <none@none> |
slight cleanup of lemmas --HG-- extra : rebase_source : 17dbf1b3c59a40c2a2ac93ab58d3e6371773af6c
|
#
1901affb |
|
18-Jul-2015 |
wenzelm <none@none> |
isabelle update_cartouches;
|
#
cd8a26ec |
|
21-Apr-2015 |
paulson <lp15@cam.ac.uk> |
New material, mostly about limits. Consolidation.
|
#
e7eb131a |
|
18-Mar-2015 |
paulson <lp15@cam.ac.uk> |
Lots of new material on complex-valued functions. Modified simplification of (x/n)^k
|
#
57ed09d5 |
|
16-Mar-2015 |
hoelzl <none@none> |
add inequalities (move from AFP/Amortized_Complexity)
|
#
b5ab68e6 |
|
05-Mar-2015 |
paulson <lp15@cam.ac.uk> |
The function frac. Various lemmas about limits, series, the exp function, etc.
|
#
c20330cc |
|
21-Nov-2014 |
Andreas Lochbihler <none@none> |
add lemma following a proof suggestion by Joachim Breitner
|
#
ff53cb2b |
|
13-Nov-2014 |
hoelzl <none@none> |
import general theorems from AFP/Markov_Models
|
#
794edf80 |
|
02-Nov-2014 |
wenzelm <none@none> |
modernized header uniformly as section;
|
#
a7682ac4 |
|
20-Oct-2014 |
hoelzl <none@none> |
add tendsto_const and tendsto_ident_at as simp and intro rules --HG-- extra : rebase_source : 22eac3c1e90ec123e3d2513334c670b5eb22d7e7
|
#
bf4e83d3 |
|
28-Jun-2014 |
haftmann <none@none> |
fact consolidation
|
#
58c27ade |
|
17-Jun-2014 |
hoelzl <none@none> |
moved lemmas from the proof of the Central Limit Theorem by Jeremy Avigad and Luke Serafin --HG-- extra : rebase_source : cd4a9d91f2d415deaa6fd3411b5402ef770d74d2
|
#
43e1aec7 |
|
30-May-2014 |
hoelzl <none@none> |
introduce more powerful reindexing rules for big operators
|
#
18c12fa6 |
|
20-May-2014 |
hoelzl <none@none> |
add various lemmas
|
#
a444e184 |
|
11-Apr-2014 |
nipkow <none@none> |
made mult_nonneg_nonneg a simp rule --HG-- extra : rebase_source : 3f70ac991fa0f02839309ce9b8f418ff53f87c36
|
#
3c2af176 |
|
02-Apr-2014 |
hoelzl <none@none> |
moved generic theorems from Complex_Analysis_Basic; fixed some theorem names
|
#
956719cb |
|
19-Mar-2014 |
paulson <lp15@cam.ac.uk> |
Some rationalisation of basic lemmas
|
#
54be58b7 |
|
19-Mar-2014 |
hoelzl <none@none> |
further renaming in Series
|
#
d6283f3b |
|
18-Mar-2014 |
hoelzl <none@none> |
fix HOL-NSA; move lemmas
|
#
4cda3a80 |
|
18-Mar-2014 |
hoelzl <none@none> |
cleanup Series: sorted according to typeclass hierarchy, use {..<_} instead of {0..<_}
|
#
f8a4dbbd |
|
17-Mar-2014 |
paulson <lp15@cam.ac.uk> |
a few new theorems
|
#
b9995ead |
|
08-Dec-2013 |
wenzelm <none@none> |
more antiquotations;
|
#
d2ef840a |
|
01-Nov-2013 |
haftmann <none@none> |
more simplification rules on unary and binary minus --HG-- extra : rebase_source : 7c88c9f33c4be8eae76f508a1a73ba79c8b769b1
|
#
68fbf665 |
|
12-Sep-2013 |
haftmann <none@none> |
tuned proofs
|
#
8d20443d |
|
25-Mar-2013 |
hoelzl <none@none> |
Series.thy is based on Limits.thy and not Deriv.thy
|
#
e73aa1e9 |
|
25-Mar-2013 |
hoelzl <none@none> |
move SEQ.thy and Lim.thy to Limits.thy
|
#
fcf7ad3e |
|
22-Mar-2013 |
hoelzl <none@none> |
clean up lemma_nest_unique and renamed to nested_sequence_unique
|
#
a1f00aa7 |
|
31-Jan-2013 |
hoelzl <none@none> |
introduce order topology
|
#
0d78ab15 |
|
03-Dec-2012 |
hoelzl <none@none> |
use filterlim in Lim and SEQ; tuned proofs
|
#
a184d6d1 |
|
25-Apr-2012 |
hoelzl <none@none> |
moved lemmas to appropriate places
|
#
8bb6233a |
|
25-Mar-2012 |
huffman <none@none> |
merged fork with new numeral representation (see NEWS)
|
#
68578b38 |
|
13-Mar-2012 |
wenzelm <none@none> |
prefer abs_def over def_raw;
|
#
7c00bf36 |
|
05-Sep-2011 |
huffman <none@none> |
modify lemma sums_group, and shorten proofs that use it
|
#
f6e8686d |
|
05-Sep-2011 |
huffman <none@none> |
generalize some lemmas
|
#
c835b01e |
|
04-Sep-2011 |
huffman <none@none> |
remove redundant lemmas about LIMSEQ
|
#
8f848cac |
|
28-Aug-2011 |
huffman <none@none> |
discontinue many legacy theorems about LIM and LIMSEQ, in favor of tendsto theorems
|
#
12431aeb |
|
18-Aug-2011 |
huffman <none@none> |
optimize some proofs
|
#
263e5d54 |
|
18-Aug-2011 |
huffman <none@none> |
remove bounded_(bi)linear locale interpretations, to avoid duplicating so many lemmas
|
#
c20fe2cc |
|
14-Mar-2011 |
hoelzl <none@none> |
generalize infinite sums
|
#
85982339 |
|
04-May-2010 |
huffman <none@none> |
make (X ----> L) an abbreviation for (X ---> L) sequentially
|
#
9333ace3 |
|
03-May-2010 |
huffman <none@none> |
remove unneeded constant Zseq
|
#
756c3e6e |
|
26-Apr-2010 |
haftmann <none@none> |
use new classes (linordered_)field_inverse_zero
|
#
f2a891d4 |
|
26-Apr-2010 |
haftmann <none@none> |
class division_ring_inverse_zero
|
#
5d17693c |
|
05-Feb-2010 |
haftmann <none@none> |
more consistent naming of type classes involving orderings (and lattices) -- c.f. NEWS
|
#
69033627 |
|
09-Nov-2009 |
wenzelm <none@none> |
eliminated hard tabulators;
|
#
a9fd0b04 |
|
28-Oct-2009 |
paulson <none@none> |
New theory Probability, which contains a development of measure theory
|
#
0b210e9b |
|
05-Oct-2009 |
paulson <none@none> |
New lemmas connected with the reals and infinite series
|
#
b9713435 |
|
25-Sep-2009 |
paulson <none@none> |
New lemmas involving the real numbers, especially limits and series
|
#
3123df1d |
|
28-May-2009 |
huffman <none@none> |
generalize constants in SEQ.thy to class metric_space
|
#
baadc210 |
|
28-Apr-2009 |
haftmann <none@none> |
stripped class recpower further
|
#
3139985e |
|
22-Mar-2009 |
nipkow <none@none> |
1. New cancellation simprocs for common factors in inequations 2. Updated the documentation
|
#
121e82fb |
|
04-Mar-2009 |
blanchet <none@none> |
Merge.
|
#
8f335aa9 |
|
24-Feb-2009 |
huffman <none@none> |
make more proofs work whether or not One_nat_def is a simp rule
|
#
92153b8c |
|
05-Feb-2009 |
hoelzl <none@none> |
Added derivation lemmas for power series and theorems for the pi, arcus tangens and logarithm series
|
#
66194568 |
|
29-Dec-2008 |
haftmann <none@none> |
adapted HOL source structure to distribution layout --HG-- rename : src/HOL/Library/Dense_Linear_Order.thy => src/HOL/Dense_Linear_Order.thy rename : src/HOL/Complex/Fundamental_Theorem_Algebra.thy => src/HOL/Fundamental_Theorem_Algebra.thy rename : src/HOL/Real/HahnBanach/Bounds.thy => src/HOL/HahnBanach/Bounds.thy rename : src/HOL/Real/HahnBanach/FunctionNorm.thy => src/HOL/HahnBanach/FunctionNorm.thy rename : src/HOL/Real/HahnBanach/FunctionOrder.thy => src/HOL/HahnBanach/FunctionOrder.thy rename : src/HOL/Real/HahnBanach/HahnBanach.thy => src/HOL/HahnBanach/HahnBanach.thy rename : src/HOL/Real/HahnBanach/HahnBanachExtLemmas.thy => src/HOL/HahnBanach/HahnBanachExtLemmas.thy rename : src/HOL/Real/HahnBanach/HahnBanachLemmas.thy => src/HOL/HahnBanach/HahnBanachLemmas.thy rename : src/HOL/Real/HahnBanach/HahnBanachSupLemmas.thy => src/HOL/HahnBanach/HahnBanachSupLemmas.thy rename : src/HOL/Real/HahnBanach/Linearform.thy => src/HOL/HahnBanach/Linearform.thy rename : src/HOL/Real/HahnBanach/NormedSpace.thy => src/HOL/HahnBanach/NormedSpace.thy rename : src/HOL/Real/HahnBanach/README.html => src/HOL/HahnBanach/README.html rename : src/HOL/Real/HahnBanach/ROOT.ML => src/HOL/HahnBanach/ROOT.ML rename : src/HOL/Real/HahnBanach/Subspace.thy => src/HOL/HahnBanach/Subspace.thy rename : src/HOL/Real/HahnBanach/VectorSpace.thy => src/HOL/HahnBanach/VectorSpace.thy rename : src/HOL/Real/HahnBanach/ZornLemma.thy => src/HOL/HahnBanach/ZornLemma.thy rename : src/HOL/Real/HahnBanach/document/root.bib => src/HOL/HahnBanach/document/root.bib rename : src/HOL/Real/HahnBanach/document/root.tex => src/HOL/HahnBanach/document/root.tex rename : src/HOL/Real/RealVector.thy => src/HOL/RealVector.thy rename : src/HOL/Hyperreal/SEQ.thy => src/HOL/SEQ.thy
|
#
f21befe1 |
|
03-Dec-2008 |
haftmann <none@none> |
made repository layout more coherent with logical distribution structure; stripped some $Id$s --HG-- rename : src/HOL/Library/Code_Message.thy => src/HOL/Code_Message.thy rename : src/HOL/Complex/Complex.thy => src/HOL/Complex.thy rename : src/HOL/Complex/Complex_Main.thy => src/HOL/Complex_Main.thy rename : src/HOL/Real/ContNotDenum.thy => src/HOL/ContNotDenum.thy rename : src/HOL/Hyperreal/Deriv.thy => src/HOL/Deriv.thy rename : src/HOL/Hyperreal/Fact.thy => src/HOL/Fact.thy rename : src/HOL/Hyperreal/FrechetDeriv.thy => src/HOL/FrechetDeriv.thy rename : src/HOL/Library/GCD.thy => src/HOL/GCD.thy rename : src/HOL/Hyperreal/Integration.thy => src/HOL/Integration.thy rename : src/HOL/Real/Float.thy => src/HOL/Library/Float.thy rename : src/HOL/Hyperreal/Lim.thy => src/HOL/Lim.thy rename : src/HOL/Hyperreal/Ln.thy => src/HOL/Ln.thy rename : src/HOL/Hyperreal/Log.thy => src/HOL/Log.thy rename : src/HOL/Real/Lubs.thy => src/HOL/Lubs.thy rename : src/HOL/Hyperreal/MacLaurin.thy => src/HOL/MacLaurin.thy rename : src/HOL/Hyperreal/NthRoot.thy => src/HOL/NthRoot.thy rename : src/HOL/Library/Order_Relation.thy => src/HOL/Order_Relation.thy rename : src/HOL/Real/PReal.thy => src/HOL/PReal.thy rename : src/HOL/Library/Parity.thy => src/HOL/Parity.thy rename : src/HOL/Real/RComplete.thy => src/HOL/RComplete.thy rename : src/HOL/Real/Rational.thy => src/HOL/Rational.thy rename : src/HOL/Real/Real.thy => src/HOL/Real.thy rename : src/HOL/Real/RealDef.thy => src/HOL/RealDef.thy rename : src/HOL/Real/RealPow.thy => src/HOL/RealPow.thy rename : src/HOL/Hyperreal/Series.thy => src/HOL/Series.thy rename : src/HOL/Hyperreal/Taylor.thy => src/HOL/Taylor.thy rename : src/HOL/arith_data.ML => src/HOL/Tools/arith_data.ML rename : src/HOL/Real/float_arith.ML => src/HOL/Tools/float_arith.ML rename : src/HOL/Real/float_syntax.ML => src/HOL/Tools/float_syntax.ML rename : src/HOL/hologic.ML => src/HOL/Tools/hologic.ML rename : src/HOL/int_arith1.ML => src/HOL/Tools/int_arith.ML rename : src/HOL/int_factor_simprocs.ML => src/HOL/Tools/int_factor_simprocs.ML rename : src/HOL/nat_simprocs.ML => src/HOL/Tools/nat_simprocs.ML rename : src/HOL/Real/rat_arith.ML => src/HOL/Tools/rat_arith.ML rename : src/HOL/Real/real_arith.ML => src/HOL/Tools/real_arith.ML rename : src/HOL/simpdata.ML => src/HOL/Tools/simpdata.ML rename : src/HOL/Hyperreal/Transcendental.thy => src/HOL/Transcendental.thy rename : src/HOL/Library/RType.thy => src/HOL/Typerep.thy rename : src/HOL/Library/Univ_Poly.thy => src/HOL/Univ_Poly.thy rename : src/HOL/Complex/ex/Arithmetic_Series_Complex.thy => src/HOL/ex/Arithmetic_Series_Complex.thy rename : src/HOL/Complex/ex/BigO_Complex.thy => src/HOL/ex/BigO_Complex.thy rename : src/HOL/Complex/ex/HarmonicSeries.thy => src/HOL/ex/HarmonicSeries.thy rename : src/HOL/Complex/ex/MIR.thy => src/HOL/ex/MIR.thy rename : src/HOL/Complex/ex/ReflectedFerrack.thy => src/HOL/ex/ReflectedFerrack.thy rename : src/HOL/Complex/ex/Sqrt.thy => src/HOL/ex/Sqrt.thy rename : src/HOL/Complex/ex/Sqrt_Script.thy => src/HOL/ex/Sqrt_Script.thy rename : src/HOL/Complex/ex/linrtac.ML => src/HOL/ex/linrtac.ML rename : src/HOL/Complex/ex/mirtac.ML => src/HOL/ex/mirtac.ML rename : src/Pure/Tools/quickcheck.ML => src/Tools/quickcheck.ML rename : src/Pure/Tools/value.ML => src/Tools/value.ML
|