| #
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
|