| Wed, 03 Jun 2009 16:56:41 +0200 |
immler |
additional debugging
|
changeset |
files
|
| Wed, 03 Jun 2009 16:56:41 +0200 |
immler |
include chain-ths in every prover-call
|
changeset |
files
|
| Wed, 03 Jun 2009 16:56:41 +0200 |
immler |
split preparing clauses and writing problemfile;
|
changeset |
files
|
| Wed, 03 Jun 2009 07:12:57 -0700 |
huffman |
merged
|
changeset |
files
|
| Tue, 02 Jun 2009 23:56:12 -0700 |
huffman |
merged
|
changeset |
files
|
| Tue, 02 Jun 2009 23:49:46 -0700 |
huffman |
instance ^ :: complete_space
|
changeset |
files
|
| Tue, 02 Jun 2009 23:35:52 -0700 |
huffman |
instance * :: complete_space; generalize continuity lemmas for fst, snd, Pair
|
changeset |
files
|
| Tue, 02 Jun 2009 23:31:03 -0700 |
huffman |
generalize type of constant lim
|
changeset |
files
|
| Tue, 02 Jun 2009 23:06:05 -0700 |
huffman |
class complete_space
|
changeset |
files
|
| Tue, 02 Jun 2009 22:35:56 -0700 |
huffman |
generalize constant uniformly_continuous_on
|
changeset |
files
|
| Tue, 02 Jun 2009 22:09:50 -0700 |
huffman |
generalize more constants
|
changeset |
files
|
| Tue, 02 Jun 2009 20:35:04 -0700 |
huffman |
generalize type of bounded
|
changeset |
files
|
| Tue, 02 Jun 2009 20:10:56 -0700 |
huffman |
generalize lemma norm_pastecart
|
changeset |
files
|
| Tue, 02 Jun 2009 19:42:44 -0700 |
huffman |
generalize lemma norm_triangle_sub
|
changeset |
files
|
| Tue, 02 Jun 2009 19:29:18 -0700 |
huffman |
generalize lemma Lim_unique
|
changeset |
files
|
| Tue, 02 Jun 2009 18:59:50 -0700 |
huffman |
generalize lemma closed_cball
|
changeset |
files
|
| Tue, 02 Jun 2009 18:46:32 -0700 |
huffman |
generalize Lim_transform lemmas
|
changeset |
files
|
| Tue, 02 Jun 2009 18:31:11 -0700 |
huffman |
generalize lemma interior_closed_Un_empty_interior
|
changeset |
files
|
| Tue, 02 Jun 2009 17:20:20 -0700 |
huffman |
reuse definition of nets from Limits.thy
|
changeset |
files
|
| Tue, 02 Jun 2009 17:03:22 -0700 |
huffman |
replace filters with filter bases
|
changeset |
files
|
| Tue, 02 Jun 2009 15:37:59 -0700 |
huffman |
generalize type of 'at' to metric_space
|
changeset |
files
|
| Tue, 02 Jun 2009 15:13:22 -0700 |
huffman |
redefine nets as filter bases
|
changeset |
files
|
| Tue, 02 Jun 2009 10:32:19 -0700 |
huffman |
new lemmas
|
changeset |
files
|
| Mon, 01 Jun 2009 16:59:56 -0700 |
huffman |
limits of Pair using filters
|
changeset |
files
|
| Wed, 03 Jun 2009 11:33:16 +0200 |
hoelzl |
Removed usage of reference in reification
|
changeset |
files
|
| Tue, 02 Jun 2009 18:38:13 +0200 |
hoelzl |
corrected spacing in reflection
|
changeset |
files
|
| Wed, 03 Jun 2009 07:51:11 +1000 |
kleing |
switch at-sml-dev-e back to full test on macbroy23
|
changeset |
files
|
| Tue, 02 Jun 2009 23:30:45 +0200 |
wenzelm |
IsabelleProcess: emit status "ready" after initialization and reports;
|
changeset |
files
|
| Tue, 02 Jun 2009 21:13:47 +0200 |
haftmann |
moved restrict_map_insert to theory Map
|
changeset |
files
|
| Tue, 02 Jun 2009 18:26:12 +0200 |
haftmann |
merged
|
changeset |
files
|
| Tue, 02 Jun 2009 18:26:01 +0200 |
haftmann |
added Landau theory
|
changeset |
files
|
| Tue, 02 Jun 2009 16:23:43 +0200 |
haftmann |
added/moved lemmas by Andreas Lochbihler
|
changeset |
files
|