| #
47185b7e |
|
10-Jul-2018 |
paulson <lp15@cam.ac.uk> |
de-applying, etc.
|
| #
7bd366c3 |
|
18-Jun-2018 |
paulson <lp15@cam.ac.uk> |
New material in support of quaternions
|
| #
48745e07 |
|
03-May-2018 |
paulson <lp15@cam.ac.uk> |
Some tidying up (mostly regarding summations from 0)
|
| #
7f370351 |
|
22-Feb-2018 |
immler <none@none> |
moved theorems from AFP/Affine_Arithmetic and AFP/Ordinary_Differential_Equations
|
| #
de79d13d |
|
08-Oct-2017 |
haftmann <none@none> |
one uniform type class for parity structures
--HG--
extra : rebase_source : edf12af006cee8d114754f4a1916094166004337
|
| #
3f30d088 |
|
22-Apr-2017 |
wenzelm <none@none> |
theories "GCD" and "Binomial" are already included in "Main": this avoids improper imports in applications;
--HG--
rename : src/HOL/Main.thy => src/HOL/Pre_Main.thy
|
| #
351cc2e6 |
|
17-Oct-2016 |
nipkow <none@none> |
setsum -> sum
|
| #
c3a11a3a |
|
10-Oct-2016 |
paulson <lp15@cam.ac.uk> |
invariance of domain
|
| #
c6fb3931 |
|
25-Aug-2016 |
Manuel Eberl <eberlm@in.tum.de> |
More analysis lemmas
|
| #
b188171c |
|
28-Jul-2016 |
wenzelm <none@none> |
misc tuning and modernization;
|
| #
14c6dd50 |
|
12-Jul-2016 |
wenzelm <none@none> |
misc tuning and modernization;
|
| #
a70bd0e1 |
|
09-Jul-2016 |
haftmann <none@none> |
more lemmas to emphasize {0::nat..(<)n} as canonical representation of intervals on nat
* * *
more rules for setsum, setprod on intervals
|
| #
b1935b2f |
|
02-Jul-2016 |
haftmann <none@none> |
simplified definitions of combinatorial functions
|
| #
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
|
| #
35f7dccd |
|
23-Feb-2016 |
nipkow <none@none> |
more canonical names
|
| #
a6f23363 |
|
17-Feb-2016 |
haftmann <none@none> |
generalized some lemmas;
moved some lemmas in more appropriate places;
deleted potentially dangerous simp rule
|
| #
2baeab22 |
|
11-Jan-2016 |
paulson <none@none> |
nonneg_Reals, nonpos_Reals, Cauchy integral formula, etc.
|
| #
82353fd1 |
|
30-Dec-2015 |
wenzelm <none@none> |
more symbols;
|
| #
6d3e0a15 |
|
29-Dec-2015 |
wenzelm <none@none> |
more symbols;
|
| #
08cabf03 |
|
27-Dec-2015 |
wenzelm <none@none> |
prefer symbols for "abs";
|
| #
420aaf4c |
|
12-Nov-2015 |
paulson <lp15@cam.ac.uk> |
Tweaks for "real": Removal of [iff] status for some lemmas, adding [simp] for others. Plus fixes.
|
| #
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.
|
| #
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;
|
| #
7d3b4baf |
|
30-Jun-2015 |
paulson <lp15@cam.ac.uk> |
Useful lemmas. The theorem concerning swapping the variables in a double integral.
|
| #
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
|
| #
794edf80 |
|
02-Nov-2014 |
wenzelm <none@none> |
modernized header uniformly as section;
|
| #
06e59c9f |
|
23-Oct-2014 |
haftmann <none@none> |
downshift of theory Parity in the hierarchy
|
| #
3c2ea5d6 |
|
19-Oct-2014 |
haftmann <none@none> |
prefer generic elimination rules for even/odd over specialized unfold rules for nat
|
| #
38907e37 |
|
05-Jul-2014 |
haftmann <none@none> |
prefer ac_simps collections over separate name bindings for add and mult
|
| #
e46c07fd |
|
04-Jul-2014 |
haftmann <none@none> |
reduced name variants for assoc and commute on plus and mult
|
| #
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
|
| #
89029f28 |
|
02-Jun-2014 |
hoelzl <none@none> |
remove superfluous assumption
|
| #
61aadd1e |
|
06-May-2014 |
hoelzl <none@none> |
avoid the Complex constructor, use the more natural Re/Im view; moved csqrt to Complex.
--HG--
extra : rebase_source : 899541490c73fe6897445f97dc2a5a3c929cf153
|
| #
a444e184 |
|
11-Apr-2014 |
nipkow <none@none> |
made mult_nonneg_nonneg a simp rule
--HG--
extra : rebase_source : 3f70ac991fa0f02839309ce9b8f418ff53f87c36
|
| #
85993f65 |
|
03-Apr-2014 |
hoelzl <none@none> |
merged DERIV_intros, has_derivative_intros into derivative_intros
|
| #
b50566a5 |
|
02-Apr-2014 |
hoelzl <none@none> |
extend continuous_intros; remove continuous_on_intros and isCont_intros
|
| #
9353bed7 |
|
06-Mar-2014 |
paulson <lp15@cam.ac.uk> |
a few new lemmas
|
| #
67c00164 |
|
12-Nov-2013 |
hoelzl <none@none> |
add finite_select_induct; move generic lemmas from MV_Analysis/Linear_Algebra to the HOL image
|
| #
b85da986 |
|
12-Sep-2013 |
huffman <none@none> |
prefer attribute 'unfolded thm' to 'simplified'
--HG--
extra : rebase_source : 426c3f0c143268e0e475a0b72a6c9db35e76b0b6
|
| #
b9bb5600 |
|
18-Aug-2013 |
wenzelm <none@none> |
more symbols;
|
| #
06329277 |
|
13-Aug-2013 |
wenzelm <none@none> |
standardized symbols via "isabelle update_sub_sup", excluding src/Pure and src/Tools/WWW_Find;
|
| #
905fec86 |
|
22-Mar-2013 |
hoelzl <none@none> |
modernized definition of root: use the_inv, handle positive and negative case uniformly, and 0-th root is constant 0
|
| #
e27ab117 |
|
22-Mar-2013 |
hoelzl <none@none> |
move continuous and continuous_on to the HOL image; isCont is an abbreviation for continuous (at x) (isCont is now restricted to a T2 space)
|
| #
d9333ba5 |
|
19-Oct-2012 |
webertj <none@none> |
Renamed {left,right}_distrib to distrib_{right,left}.
|
| #
af75163e |
|
10-Oct-2012 |
wenzelm <none@none> |
eliminated spurious fact duplicates;
|
| #
41c4f43b |
|
20-Aug-2011 |
huffman <none@none> |
remove redundant lemma real_0_le_divide_iff in favor or zero_le_divide_iff
|
| #
7584e614 |
|
19-Aug-2011 |
huffman <none@none> |
remove some redundant simp rules about sqrt
|
| #
12431aeb |
|
18-Aug-2011 |
huffman <none@none> |
optimize some proofs
|
| #
aaaa7964 |
|
18-Feb-2010 |
huffman <none@none> |
get rid of many duplicate simp rule warnings
|
| #
1a14d4c7 |
|
30-Jun-2009 |
hoelzl <none@none> |
Added DERIV_intros
|
| #
1487c746 |
|
28-Apr-2009 |
haftmann <none@none> |
collected square lemmas in Nat_Numeral
|
| #
8ee53001 |
|
04-Mar-2009 |
huffman <none@none> |
declare power_Suc [simp]; remove redundant type-specific versions of power_Suc
|
| #
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
|