| #
a4784f6f |
|
09-Oct-2019 |
haftmann <none@none> |
dedicated fact collections for algebraic simplification rules potentially splitting goals
--HG--
extra : rebase_source : ebbd8d0c13409f8fb536c42910e904c24e43dbe6
|
| #
efe4ca34 |
|
29-Dec-2018 |
nipkow <none@none> |
capitalize proper names in lemma names
|
| #
99a68090 |
|
20-Sep-2018 |
paulson <lp15@cam.ac.uk> |
removal of more redundancies, and fixes
|
| #
11e8aae1 |
|
20-Sep-2018 |
paulson <lp15@cam.ac.uk> |
elimination of near duplication involving Rolle's theorem and the MVT
|
| #
771cb655 |
|
21-Jul-2018 |
paulson <lp15@cam.ac.uk> |
fixing a theorem statement, etc.
|
| #
830577aa |
|
21-Jul-2018 |
paulson <lp15@cam.ac.uk> |
de-applying and removing junk
|
| #
8280abe0 |
|
12-May-2018 |
haftmann <none@none> |
removed some non-essential rules
|
| #
c7cc1919 |
|
26-Nov-2017 |
wenzelm <none@none> |
more symbols;
|
| #
1e533d09 |
|
16-Mar-2017 |
paulson <lp15@cam.ac.uk> |
Removal of [simp] status for greaterThan_0. Moved two theorems into main HOL.
|
| #
351cc2e6 |
|
17-Oct-2016 |
nipkow <none@none> |
setsum -> sum
|
| #
80cec798 |
|
31-Jul-2016 |
wenzelm <none@none> |
simplified theory structure;
|
| #
fbcfe7d0 |
|
31-Jul-2016 |
wenzelm <none@none> |
misc tuning and modernization;
|
| #
0f0a91d1 |
|
02-Jul-2016 |
haftmann <none@none> |
more theorems
|
| #
a2bc0021 |
|
25-Apr-2016 |
wenzelm <none@none> |
eliminated old 'def';
tuned comments;
|
| #
d42838c4 |
|
28-Dec-2015 |
wenzelm <none@none> |
more symbols;
|
| #
08cabf03 |
|
27-Dec-2015 |
wenzelm <none@none> |
prefer symbols for "abs";
|
| #
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.
|
| #
ae913163 |
|
30-Sep-2015 |
paulson <lp15@cam.ac.uk> |
real_of_nat_Suc is now a simprule
|
| #
85ed9565 |
|
01-Sep-2015 |
wenzelm <none@none> |
eliminated \<Colon>;
|
| #
1901affb |
|
18-Jul-2015 |
wenzelm <none@none> |
isabelle update_cartouches;
|
| #
d6db773a |
|
11-Apr-2015 |
paulson <lp15@cam.ac.uk> |
Overloading of ln and powr, but "approximation" no longer works for powr. Code generation also fails due to type ambiguity in scala.
|
| #
3e14dd10 |
|
16-Mar-2015 |
paulson <lp15@cam.ac.uk> |
The factorial function, "fact", now has type "nat => 'a"
|
| #
794edf80 |
|
02-Nov-2014 |
wenzelm <none@none> |
modernized header uniformly as section;
|
| #
3c2ea5d6 |
|
19-Oct-2014 |
haftmann <none@none> |
prefer generic elimination rules for even/odd over specialized unfold rules for nat
|
| #
6a02610c |
|
21-Sep-2014 |
haftmann <none@none> |
explicit separation of signed and unsigned numerals using existing lexical categories num and xnum
|
| #
38907e37 |
|
05-Jul-2014 |
haftmann <none@none> |
prefer ac_simps collections over separate name bindings for add and mult
|
| #
bf4e83d3 |
|
28-Jun-2014 |
haftmann <none@none> |
fact consolidation
|
| #
9fd71573 |
|
10-Jun-2014 |
Thomas Sewell <thomas.sewell@nicta.com.au> |
Hypsubst preserves equality hypotheses
Fixes included for various theories affected by this change.
--HG--
extra : rebase_source : b0150e06a14c2821e03208834282be6eca87aae0
|
| #
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
|
| #
52d226b9 |
|
21-Mar-2014 |
paulson <lp15@cam.ac.uk> |
a few new lemmas and generalisations of old ones
|
| #
4cda3a80 |
|
18-Mar-2014 |
hoelzl <none@none> |
cleanup Series: sorted according to typeclass hierarchy, use {..<_} instead of {0..<_}
|
| #
e52c6f99 |
|
17-Mar-2014 |
hoelzl <none@none> |
unify syntax for has_derivative and differentiable
|
| #
d4cae3bf |
|
23-Mar-2013 |
haftmann <none@none> |
fundamental revision of big operators on sets
|
| #
d9333ba5 |
|
19-Oct-2012 |
webertj <none@none> |
Renamed {left,right}_distrib to distrib_{right,left}.
|
| #
ad9e459c |
|
11-Sep-2011 |
nipkow <none@none> |
new fastforce replacing fastsimp - less confusing name
|
| #
19dfe100 |
|
19-Aug-2011 |
huffman <none@none> |
move sin_coeff and cos_coeff lemmas to Transcendental.thy; simplify some proofs
|
| #
564cc792 |
|
19-Aug-2011 |
huffman <none@none> |
Transcendental.thy: remove several unused lemmas and simplify some proofs
|
| #
afcdf510 |
|
19-Aug-2011 |
huffman <none@none> |
fold definitions of sin_coeff and cos_coeff in Maclaurin lemmas
|
| #
b74d1b75 |
|
15-Dec-2010 |
hoelzl <none@none> |
beautify MacLaurin proofs; make better use of DERIV_intros
|
| #
fb592554 |
|
15-Dec-2010 |
bulwahn <none@none> |
adding an Isar version of the MacLaurin theorem from some students' work in 2005
|
| #
fe5bdb56 |
|
17-May-2010 |
huffman <none@none> |
remove some unnamed simp rules from Transcendental.thy; move the needed ones to MacLaurin.thy where they are used
|
| #
f1682097 |
|
17-Jul-2009 |
avigad <none@none> |
Changed fact_Suc_nat back to fact_Suc
|
| #
eea8493a |
|
09-Jul-2009 |
avigad <none@none> |
Repaired uses of factorial.
|
| #
0e77d8f9 |
|
30-Jun-2009 |
hoelzl <none@none> |
remove DERIV_tac and deriv_tac, neither is used in Isabelle/HOL or the AFP
|
| #
f6a321d1 |
|
30-Jun-2009 |
hoelzl <none@none> |
use DERIV_intros
|
| #
869ba495 |
|
14-May-2009 |
nipkow <none@none> |
Cleaned up Parity a little
|
| #
8ee53001 |
|
04-Mar-2009 |
huffman <none@none> |
declare power_Suc [simp]; remove redundant type-specific versions of power_Suc
|
| #
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
|
| #
98296995 |
|
05-Feb-2009 |
chaieb@chaieb-laptop <chaieb@chaieb-laptop> |
fixed Proofs and dependencies ; Theory Dense_Linear_Order moved to Library
|
| #
92153b8c |
|
05-Feb-2009 |
hoelzl <none@none> |
Added derivation lemmas for power series and theorems for the pi, arcus tangens and logarithm series
|
| #
6df62472 |
|
28-Dec-2008 |
huffman <none@none> |
clean up proofs of lemma Maclaurin
|
| #
7f02b33f |
|
24-Dec-2008 |
huffman <none@none> |
use less_iff_Suc_add instead of less_add_one
|
| #
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
|