Sat, 20 Aug 2011 16:06:27 +0200 |
wenzelm |
clarified fulfill_norm_proof: no join_thms yet;
|
changeset |
files
|
Sat, 20 Aug 2011 15:52:29 +0200 |
wenzelm |
added Future.joins convenience;
|
changeset |
files
|
Sat, 20 Aug 2011 09:42:34 +0200 |
haftmann |
merged
|
changeset |
files
|
Sat, 20 Aug 2011 09:42:12 +0200 |
haftmann |
deactivated »unknown« nitpick example
|
changeset |
files
|
Sat, 20 Aug 2011 09:30:23 +0200 |
haftmann |
merged
|
changeset |
files
|
Sat, 20 Aug 2011 01:40:22 +0200 |
haftmann |
tuned proof
|
changeset |
files
|
Sat, 20 Aug 2011 01:39:27 +0200 |
haftmann |
more uniform formatting of specifications
|
changeset |
files
|
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
|