| Sat, 16 Dec 2006 20:23:45 +0100 |
huffman |
moved several theorems; rearranged theory dependencies
|
changeset |
files
|
| Sat, 16 Dec 2006 19:37:07 +0100 |
huffman |
hypreal_of_hypnat abbreviates more general of_hypnat
|
changeset |
files
|
| Fri, 15 Dec 2006 17:51:07 +0100 |
webertj |
tracing instead of warning
|
changeset |
files
|
| Fri, 15 Dec 2006 00:08:50 +0100 |
wenzelm |
updated;
|
changeset |
files
|
| Fri, 15 Dec 2006 00:08:16 +0100 |
wenzelm |
removed obsolete assert;
|
changeset |
files
|
| Fri, 15 Dec 2006 00:08:15 +0100 |
wenzelm |
renamed LocalTheory.assert to affirm;
|
changeset |
files
|
| Fri, 15 Dec 2006 00:08:14 +0100 |
wenzelm |
tuned -- accomodate Alice;
|
changeset |
files
|
| Fri, 15 Dec 2006 00:08:06 +0100 |
wenzelm |
avoid conflict with Alice keywords: renamed pack -> implode, unpack -> explode, any -> many, avoided assert;
|
changeset |
files
|
| Thu, 14 Dec 2006 22:19:39 +0100 |
huffman |
remove Hyperreal/fuf.ML
|
changeset |
files
|
| Thu, 14 Dec 2006 22:18:08 +0100 |
huffman |
remove commented section
|
changeset |
files
|
| Thu, 14 Dec 2006 22:09:26 +0100 |
huffman |
remove ultra tactic and redundant FreeUltrafilterNat lemmas
|
changeset |
files
|
| Thu, 14 Dec 2006 22:08:35 +0100 |
huffman |
declare insert_iff [simp]
|
changeset |
files
|
| Thu, 14 Dec 2006 21:46:59 +0100 |
wenzelm |
activated improved use_ml, which captures output and reports source positions;
|
changeset |
files
|
| Thu, 14 Dec 2006 21:46:58 +0100 |
wenzelm |
tuned;
|
changeset |
files
|
| Thu, 14 Dec 2006 21:33:47 +0100 |
huffman |
prove hyperpow_realpow using transfer
|
changeset |
files
|