| Tue, 15 May 2007 05:09:01 +0200 |
huffman |
remove simp attribute from various polar_Ex lemmas
|
changeset |
files
|
| Mon, 14 May 2007 23:25:16 +0200 |
huffman |
tuned proofs
|
changeset |
files
|
| Mon, 14 May 2007 23:09:54 +0200 |
huffman |
spelling: rename arcos -> arccos
|
changeset |
files
|
| Mon, 14 May 2007 22:32:51 +0200 |
huffman |
tuned proofs
|
changeset |
files
|
| Mon, 14 May 2007 20:48:32 +0200 |
huffman |
add lemma sgn_mult; declare real_scaleR_def and scaleR_eq_0_iff as simp rules
|
changeset |
files
|
| Mon, 14 May 2007 20:14:31 +0200 |
huffman |
generalized sgn function to work on any real normed vector space
|
changeset |
files
|
| Mon, 14 May 2007 19:14:50 +0200 |
huffman |
root and sqrt on negative inputs
|
changeset |
files
|
| Mon, 14 May 2007 18:48:24 +0200 |
huffman |
move lemmas to RealPow.thy; tuned proofs
|
changeset |
files
|
| Mon, 14 May 2007 18:04:52 +0200 |
huffman |
tuned proofs
|
changeset |
files
|
| Mon, 14 May 2007 18:03:25 +0200 |
huffman |
tuned
|
changeset |
files
|
| Mon, 14 May 2007 17:45:42 +0200 |
huffman |
added general sum-squares lemmas
|
changeset |
files
|
| Mon, 14 May 2007 17:37:31 +0200 |
huffman |
new lemmas
|
changeset |
files
|
| Mon, 14 May 2007 13:24:22 +0200 |
webertj |
ProofGeneral: Find Theorems search form
|
changeset |
files
|
| Mon, 14 May 2007 12:52:56 +0200 |
haftmann |
reorganized float arithmetic
|
changeset |
files
|
| Mon, 14 May 2007 12:52:54 +0200 |
haftmann |
fixed IntInf ambiguity
|
changeset |
files
|
| Mon, 14 May 2007 09:33:18 +0200 |
huffman |
remove redundant lemmas
|
changeset |
files
|
| Mon, 14 May 2007 09:27:24 +0200 |
huffman |
remove redundant lemmas
|
changeset |
files
|
| Mon, 14 May 2007 09:16:47 +0200 |
huffman |
remove redundant lemmas
|
changeset |
files
|
| Mon, 14 May 2007 09:11:30 +0200 |
huffman |
remove redundant lemmas
|
changeset |
files
|
| Mon, 14 May 2007 08:15:13 +0200 |
huffman |
cleaned up
|
changeset |
files
|
| Mon, 14 May 2007 08:12:38 +0200 |
huffman |
tuned
|
changeset |
files
|
| Sun, 13 May 2007 20:05:42 +0200 |
huffman |
define roots of negative reals so that many lemmas no longer require side conditions; simplification solves more goals than previously
|
changeset |
files
|
| Sun, 13 May 2007 19:15:36 +0200 |
huffman |
add lemma power_eq_imp_eq_base
|
changeset |
files
|
| Sun, 13 May 2007 18:16:49 +0200 |
haftmann |
added module int
|
changeset |
files
|