| Thu, 03 Jul 2008 20:53:44 +0200 |
huffman |
use real_of_nat_ge_zero instead of real_of_nat_fact_ge_zero
|
file |
diff |
annotate
|
| Wed, 09 Jan 2008 19:23:50 +0100 |
nipkow |
added simp attributes/ proofs fixed
|
file |
diff |
annotate
|
| Sun, 24 Jun 2007 20:55:41 +0200 |
nipkow |
tuned and used field_simps
|
file |
diff |
annotate
|
| Sat, 23 Jun 2007 19:33:22 +0200 |
nipkow |
tuned and renamed group_eq_simps and ring_eq_simps
|
file |
diff |
annotate
|
| Wed, 20 Jun 2007 19:49:14 +0200 |
huffman |
avoid using implicit prems in assumption
|
file |
diff |
annotate
|
| Mon, 28 May 2007 16:27:33 +0200 |
huffman |
add type annotations for exp
|
file |
diff |
annotate
|
| Thu, 17 May 2007 21:51:32 +0200 |
huffman |
avoid using redundant lemmas from RealDef.thy
|
file |
diff |
annotate
|
| Fri, 13 Apr 2007 00:48:12 +0200 |
huffman |
new simp rule exp_ln; new standard proof of DERIV_exp_ln_one; changed imports
|
file |
diff |
annotate
|
| Sun, 24 Sep 2006 05:49:50 +0200 |
huffman |
generalized types of sums, summable, and suminf
|
file |
diff |
annotate
|
| Mon, 18 Sep 2006 07:48:07 +0200 |
huffman |
replace (x + - y) with (x - y)
|
file |
diff |
annotate
|
| Wed, 30 Aug 2006 03:19:08 +0200 |
webertj |
lin_arith_prover: splitting reverted because of performance loss
|
file |
diff |
annotate
|
| Sun, 30 Jul 2006 05:53:10 +0200 |
webertj |
lin_arith_prover splits certain operators (e.g. min, max, abs)
|
file |
diff |
annotate
|
| Fri, 02 Jun 2006 23:22:29 +0200 |
wenzelm |
misc cleanup;
|
file |
diff |
annotate
|
| Wed, 03 Aug 2005 14:48:42 +0200 |
avigad |
renamed exp_ge_add_one_self2 to exp_ge_add_one_self
|
file |
diff |
annotate
|
| Sat, 30 Jul 2005 16:50:55 +0200 |
nipkow |
addedd ID line
|
file |
diff |
annotate
|
| Fri, 29 Jul 2005 19:47:19 +0200 |
avigad |
added a new theory; properties of ln
|
file |
diff |
annotate
|