| Sun, 24 Sep 2006 04:00:46 +0200 |
huffman |
remove extra dependencies
|
changeset |
files
|
| Sun, 24 Sep 2006 04:00:03 +0200 |
huffman |
add proof of summable_LIMSEQ_zero
|
changeset |
files
|
| Sun, 24 Sep 2006 03:38:36 +0200 |
huffman |
change definitions from SOME to THE
|
changeset |
files
|
| Sun, 24 Sep 2006 02:56:59 +0200 |
huffman |
move root and sqrt stuff from Transcendental to NthRoot
|
changeset |
files
|
| Sun, 24 Sep 2006 01:04:44 +0200 |
huffman |
fix proof
|
changeset |
files
|
| Fri, 22 Sep 2006 23:19:45 +0200 |
huffman |
added lemmas about LIMSEQ and norm; simplified some proofs
|
changeset |
files
|
| Fri, 22 Sep 2006 23:17:39 +0200 |
huffman |
add lemma norm_power
|
changeset |
files
|
| Fri, 22 Sep 2006 21:42:12 +0200 |
wenzelm |
added HOL-Complex-ex;
|
changeset |
files
|
| Fri, 22 Sep 2006 16:25:15 +0200 |
huffman |
define constants with THE instead of SOME
|
changeset |
files
|
| Fri, 22 Sep 2006 14:36:23 +0200 |
berghofe |
Fixed bug concerning the generation of identifiers for
|
changeset |
files
|
| Fri, 22 Sep 2006 14:32:46 +0200 |
berghofe |
Replaced irreducible_paths by all_paths.
|
changeset |
files
|
| Fri, 22 Sep 2006 14:30:37 +0200 |
berghofe |
Added function all_paths (formerly find_paths).
|
changeset |
files
|
| Fri, 22 Sep 2006 13:04:30 +0200 |
wenzelm |
tuned proofs;
|
changeset |
files
|
| Thu, 21 Sep 2006 19:06:16 +0200 |
wenzelm |
tuned oracle name;
|
changeset |
files
|