Sun, 25 Mar 2012 20:15:39 +0200 
huffman 
merged fork with new numeral representation (see NEWS)

file 
diff 
annotate

Tue, 17 Jan 2012 16:30:54 +0100 
huffman 
factorcancellation simprocs now call the full simplifier to prove that factors are nonzero

file 
diff 
annotate

Thu, 15 Dec 2011 17:21:29 +0100 
huffman 
tendsto lemmas for ln and powr

file 
diff 
annotate

Sun, 30 Oct 2011 09:42:13 +0100 
huffman 
removed adhoc simp rules sin_cos_eq[symmetric], minus_sin_cos_eq[symmetric], cos_sin_eq[symmetric]

file 
diff 
annotate

Sun, 30 Oct 2011 09:07:02 +0100 
huffman 
extend cancellation simproc patterns to cover terms like ' (2 * pi) < pi'

file 
diff 
annotate

Tue, 06 Sep 2011 10:30:00 0700 
huffman 
simplify proof of tan_half, removing unused assumptions

file 
diff 
annotate

Tue, 06 Sep 2011 09:56:09 0700 
huffman 
convert some proofs to Isarstyle

file 
diff 
annotate

Mon, 05 Sep 2011 22:30:25 0700 
huffman 
add lemmas about arctan;

file 
diff 
annotate

Mon, 05 Sep 2011 18:06:02 0700 
huffman 
convert lemma cos_total to Isarstyle proof

file 
diff 
annotate

Mon, 05 Sep 2011 17:45:37 0700 
huffman 
convert lemma cos_is_zero to Isarstyle

file 
diff 
annotate

Mon, 05 Sep 2011 17:00:56 0700 
huffman 
convert lemma sin_gt_zero to Isar style;

file 
diff 
annotate

Mon, 05 Sep 2011 16:26:57 0700 
huffman 
modify lemma sums_group, and shorten proofs that use it

file 
diff 
annotate

Mon, 05 Sep 2011 16:07:40 0700 
huffman 
generalize some lemmas

file 
diff 
annotate

Mon, 05 Sep 2011 12:19:04 0700 
huffman 
add lemmas cos_arctan and sin_arctan

file 
diff 
annotate

Sun, 04 Sep 2011 09:49:45 0700 
huffman 
remove redundant lemmas about LIMSEQ

file 
diff 
annotate

Sun, 28 Aug 2011 09:20:12 0700 
huffman 
discontinue many legacy theorems about LIM and LIMSEQ, in favor of tendsto theorems

file 
diff 
annotate

Fri, 19 Aug 2011 18:42:41 0700 
huffman 
move sin_coeff and cos_coeff lemmas to Transcendental.thy; simplify some proofs

file 
diff 
annotate

Fri, 19 Aug 2011 18:08:05 0700 
huffman 
remove unused lemma DERIV_sin_add

file 
diff 
annotate

Fri, 19 Aug 2011 18:06:27 0700 
huffman 
remove redundant lemma lemma_DERIV_subst in favor of DERIV_cong

file 
diff 
annotate

Fri, 19 Aug 2011 17:59:19 0700 
huffman 
remove redundant lemma exp_ln_eq in favor of ln_unique

file 
diff 
annotate

Fri, 19 Aug 2011 14:17:28 0700 
huffman 
Transcendental.thy: add tendsto_intros lemmas;

file 
diff 
annotate

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 realspecific 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 tabwidth;

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

Wed, 27 May 2009 16:39:22 0700 
huffman 
add constants sin_coeff, cos_coeff

file 
diff 
annotate

Thu, 14 May 2009 15:39:15 +0200 
nipkow 
Cleaned up Parity a little

file 
diff 
annotate

Tue, 28 Apr 2009 15:50:30 +0200 
haftmann 
stripped class recpower further

file 
diff 
annotate

Wed, 04 Mar 2009 17:12:23 0800 
huffman 
declare power_Suc [simp]; remove redundant typespecific versions of power_Suc

file 
diff 
annotate

Tue, 24 Feb 2009 11:12:58 0800 
huffman 
make more proofs work whether or not One_nat_def is a simp rule

file 
diff 
annotate

Thu, 05 Feb 2009 11:34:42 +0100 
hoelzl 
Added derivation lemmas for power series and theorems for the pi, arcus tangens and logarithm series

file 
diff 
annotate

Fri, 30 Jan 2009 12:48:57 +0000 
chaieb 
Added real related theorems from Fact.thy

file 
diff 
annotate

Wed, 28 Jan 2009 16:29:16 +0100 
nipkow 
Replaced group_ and ring_simps by algebra_simps;

file 
diff 
annotate

Wed, 24 Dec 2008 13:29:49 0800 
huffman 
clean up lemmas about ln

file 
diff 
annotate
