| Fri, 19 Aug 2011 10:46:54 -0700 |
huffman |
Transcendental.thy: remove several unused lemmas and simplify some proofs
|
file |
diff |
annotate
|
| Fri, 19 Aug 2011 08:40:15 -0700 |
huffman |
remove unused lemmas
|
file |
diff |
annotate
|
| Fri, 19 Aug 2011 07:45:22 -0700 |
huffman |
remove some redundant simp rules
|
file |
diff |
annotate
|
| Thu, 18 Aug 2011 19:53:03 -0700 |
huffman |
optimize some proofs
|
file |
diff |
annotate
|
| Thu, 18 Aug 2011 13:36:58 -0700 |
huffman |
remove bounded_(bi)linear locale interpretations, to avoid duplicating so many lemmas
|
file |
diff |
annotate
|
| Tue, 31 May 2011 21:33:49 +0200 |
hoelzl |
use divide instead of inverse for the derivative of ln
|
file |
diff |
annotate
|
| Mon, 14 Mar 2011 14:37:35 +0100 |
hoelzl |
generalize infinite sums
|
file |
diff |
annotate
|
| Fri, 14 Jan 2011 15:44:47 +0100 |
wenzelm |
eliminated global prems;
|
file |
diff |
annotate
|
| Mon, 23 Aug 2010 11:17:13 +0200 |
haftmann |
dropped type classes mult_mono and mult_mono1; tuned names of technical rule duplicates
|
file |
diff |
annotate
|
| Mon, 19 Jul 2010 16:09:44 +0200 |
haftmann |
diff_minus subsumes diff_def
|
file |
diff |
annotate
|
| Mon, 17 May 2010 15:58:32 -0700 |
huffman |
remove some unnamed simp rules from Transcendental.thy; move the needed ones to MacLaurin.thy where they are used
|
file |
diff |
annotate
|
| Mon, 17 May 2010 08:45:46 -0700 |
huffman |
remove simp attribute from square_eq_1_iff
|
file |
diff |
annotate
|
| Tue, 11 May 2010 19:38:16 -0700 |
huffman |
fix some linarith_split_limit warnings
|
file |
diff |
annotate
|
| Tue, 11 May 2010 06:30:48 -0700 |
huffman |
move some theorems from RealPow.thy to Transcendental.thy
|
file |
diff |
annotate
|
| Sun, 09 May 2010 17:47:43 -0700 |
huffman |
avoid using real-specific versions of generic lemmas
|
file |
diff |
annotate
|
| Sun, 09 May 2010 14:21:44 -0700 |
huffman |
remove a couple of redundant lemmas; simplify some proofs
|
file |
diff |
annotate
|
| Thu, 18 Feb 2010 14:21:44 -0800 |
huffman |
get rid of many duplicate simp rule warnings
|
file |
diff |
annotate
|
| Thu, 18 Feb 2010 08:08:51 -0800 |
huffman |
fix looping call to simplifier
|
file |
diff |
annotate
|
| Mon, 08 Feb 2010 14:06:58 +0100 |
haftmann |
more precise proofs
|
file |
diff |
annotate
|
| Fri, 05 Feb 2010 14:33:50 +0100 |
haftmann |
more consistent naming of type classes involving orderings (and lattices) -- c.f. NEWS
|
file |
diff |
annotate
|
| Thu, 28 Jan 2010 11:48:49 +0100 |
haftmann |
new theory Algebras.thy for generic algebraic structures
|
file |
diff |
annotate
|
| Fri, 13 Nov 2009 17:15:12 +0000 |
paulson |
A little rationalisation
|
file |
diff |
annotate
|
| Tue, 10 Nov 2009 14:38:06 +0100 |
wenzelm |
tuned proofs;
|
file |
diff |
annotate
|
| Sat, 17 Oct 2009 14:43:18 +0200 |
wenzelm |
eliminated hard tabulators, guessing at each author's individual tab-width;
|
file |
diff |
annotate
|
| Fri, 17 Jul 2009 13:12:18 -0400 |
avigad |
Changed fact_Suc_nat back to fact_Suc
|
file |
diff |
annotate
|
| Fri, 10 Jul 2009 10:45:30 -0400 |
avigad |
Moved factorial lemmas from Binomial.thy to Fact.thy and merged.
|
file |
diff |
annotate
|
| Tue, 30 Jun 2009 18:21:55 +0200 |
hoelzl |
use DERIV_intros
|
file |
diff |
annotate
|
| Tue, 30 Jun 2009 18:16:22 +0200 |
hoelzl |
Added DERIV_intros
|
file |
diff |
annotate
|
| Wed, 24 Jun 2009 09:41:14 +0200 |
nipkow |
corrected and unified thm names
|
file |
diff |
annotate
|
| Fri, 29 May 2009 09:22:56 -0700 |
huffman |
generalize constants from Lim.thy to class metric_space
|
file |
diff |
annotate
|