2010-08-23 |
haftmann |
dropped type classes mult_mono and mult_mono1; tuned names of technical rule duplicates
|
file |
diff |
annotate
|
2010-07-19 |
haftmann |
diff_minus subsumes diff_def
|
file |
diff |
annotate
|
2010-05-17 |
huffman |
remove some unnamed simp rules from Transcendental.thy; move the needed ones to MacLaurin.thy where they are used
|
file |
diff |
annotate
|
2010-05-17 |
huffman |
remove simp attribute from square_eq_1_iff
|
file |
diff |
annotate
|
2010-05-12 |
huffman |
fix some linarith_split_limit warnings
|
file |
diff |
annotate
|
2010-05-11 |
huffman |
move some theorems from RealPow.thy to Transcendental.thy
|
file |
diff |
annotate
|
2010-05-10 |
huffman |
avoid using real-specific versions of generic lemmas
|
file |
diff |
annotate
|
2010-05-09 |
huffman |
remove a couple of redundant lemmas; simplify some proofs
|
file |
diff |
annotate
|
2010-02-18 |
huffman |
get rid of many duplicate simp rule warnings
|
file |
diff |
annotate
|
2010-02-18 |
huffman |
fix looping call to simplifier
|
file |
diff |
annotate
|
2010-02-08 |
haftmann |
more precise proofs
|
file |
diff |
annotate
|
2010-02-05 |
haftmann |
more consistent naming of type classes involving orderings (and lattices) -- c.f. NEWS
|
file |
diff |
annotate
|
2010-01-28 |
haftmann |
new theory Algebras.thy for generic algebraic structures
|
file |
diff |
annotate
|
2009-11-13 |
paulson |
A little rationalisation
|
file |
diff |
annotate
|
2009-11-10 |
wenzelm |
tuned proofs;
|
file |
diff |
annotate
|
2009-10-17 |
wenzelm |
eliminated hard tabulators, guessing at each author's individual tab-width;
|
file |
diff |
annotate
|
2009-07-17 |
avigad |
Changed fact_Suc_nat back to fact_Suc
|
file |
diff |
annotate
|
2009-07-10 |
avigad |
Moved factorial lemmas from Binomial.thy to Fact.thy and merged.
|
file |
diff |
annotate
|
2009-06-30 |
hoelzl |
use DERIV_intros
|
file |
diff |
annotate
|
2009-06-30 |
hoelzl |
Added DERIV_intros
|
file |
diff |
annotate
|
2009-06-24 |
nipkow |
corrected and unified thm names
|
file |
diff |
annotate
|
2009-05-29 |
huffman |
generalize constants from Lim.thy to class metric_space
|
file |
diff |
annotate
|
2009-05-27 |
huffman |
add constants sin_coeff, cos_coeff
|
file |
diff |
annotate
|
2009-05-14 |
nipkow |
Cleaned up Parity a little
|
file |
diff |
annotate
|
2009-04-28 |
haftmann |
stripped class recpower further
|
file |
diff |
annotate
|
2009-03-05 |
huffman |
declare power_Suc [simp]; remove redundant type-specific versions of power_Suc
|
file |
diff |
annotate
|
2009-02-24 |
huffman |
make more proofs work whether or not One_nat_def is a simp rule
|
file |
diff |
annotate
|
2009-02-05 |
hoelzl |
Added derivation lemmas for power series and theorems for the pi, arcus tangens and logarithm series
|
file |
diff |
annotate
|
2009-01-30 |
chaieb |
Added real related theorems from Fact.thy
|
file |
diff |
annotate
|
2009-01-28 |
nipkow |
Replaced group_ and ring_simps by algebra_simps;
|
file |
diff |
annotate
|
2008-12-24 |
huffman |
clean up lemmas about ln
|
file |
diff |
annotate
|
2008-12-24 |
huffman |
clean up lemmas about exp
|
file |
diff |
annotate
|
2008-12-24 |
huffman |
rearranged subsections; cleaned up some proofs
|
file |
diff |
annotate
|
2008-12-24 |
huffman |
move theorems about limits from Transcendental.thy to Deriv.thy
|
file |
diff |
annotate
|
2008-12-24 |
huffman |
cleaned up some proofs; removed redundant simp rules
|
file |
diff |
annotate
|
2008-12-23 |
huffman |
move sin and cos to their own subsection
|
file |
diff |
annotate
|
2008-12-23 |
huffman |
clean up some proofs; remove unused lemmas
|
file |
diff |
annotate
|
2008-12-03 |
haftmann |
made repository layout more coherent with logical distribution structure; stripped some $Id$s
|
file |
diff |
annotate
| base
|