| Sat, 20 Aug 2011 01:33:58 +0200 |
haftmann |
compatibility layer
|
changeset |
files
|
| Sat, 20 Aug 2011 01:21:22 +0200 |
haftmann |
merged
|
changeset |
files
|
| Fri, 19 Aug 2011 19:33:31 +0200 |
haftmann |
more concise definition for Inf, Sup on bool
|
changeset |
files
|
| Thu, 18 Aug 2011 13:37:41 +0200 |
noschinl |
do not call ghc with -fglasgow-exts
|
changeset |
files
|
| Fri, 19 Aug 2011 19:01:00 -0700 |
huffman |
remove some redundant simp rules about sqrt
|
changeset |
files
|
| Fri, 19 Aug 2011 18:42:41 -0700 |
huffman |
move sin_coeff and cos_coeff lemmas to Transcendental.thy; simplify some proofs
|
changeset |
files
|
| Fri, 19 Aug 2011 18:08:05 -0700 |
huffman |
remove unused lemma DERIV_sin_add
|
changeset |
files
|
| Fri, 19 Aug 2011 18:06:27 -0700 |
huffman |
remove redundant lemma lemma_DERIV_subst in favor of DERIV_cong
|
changeset |
files
|
| Fri, 19 Aug 2011 17:59:19 -0700 |
huffman |
remove redundant lemma exp_ln_eq in favor of ln_unique
|
changeset |
files
|
| Fri, 19 Aug 2011 16:55:43 -0700 |
huffman |
merged
|
changeset |
files
|
| Fri, 19 Aug 2011 15:54:43 -0700 |
huffman |
Lim.thy: legacy theorems
|
changeset |
files
|
| Fri, 19 Aug 2011 15:07:10 -0700 |
huffman |
SEQ.thy: legacy theorem names
|
changeset |
files
|