| Tue, 27 Jan 2009 15:47:22 +0100 |
wenzelm |
plain non-dependent types;
|
changeset |
files
|
| Tue, 27 Jan 2009 15:22:46 +0100 |
wenzelm |
turned IsarDocument into trait for IsabelleProcess;
|
changeset |
files
|
| Tue, 27 Jan 2009 14:45:52 +0100 |
wenzelm |
HOL_USEDIR_OPTIONS: -Q false, giving up parallel proofs for now due to memory shortage;
|
changeset |
files
|
| Tue, 27 Jan 2009 14:28:51 +0100 |
wenzelm |
thm_proof: recovered single-threaded version;
|
changeset |
files
|
| Tue, 27 Jan 2009 13:52:32 +0100 |
wenzelm |
merged
|
changeset |
files
|
| Tue, 27 Jan 2009 13:41:45 +0100 |
wenzelm |
recovered example types from WordMain.thy;
|
changeset |
files
|
| Tue, 27 Jan 2009 12:59:38 +0100 |
wenzelm |
merged
|
changeset |
files
|
| Tue, 27 Jan 2009 12:59:22 +0100 |
wenzelm |
added share_common_data -- reduces heap space, but takes long;
|
changeset |
files
|
| Tue, 27 Jan 2009 12:57:24 +0100 |
wenzelm |
use https;
|
changeset |
files
|
| Tue, 27 Jan 2009 00:42:12 +0100 |
wenzelm |
thm_proof: replaced lazy by composed futures;
|
changeset |
files
|
| Tue, 27 Jan 2009 00:29:37 +0100 |
wenzelm |
proof_body: turned lazy into future -- ensures that body is fulfilled eventually, without explicit force;
|
changeset |
files
|
| Mon, 26 Jan 2009 22:15:35 +0100 |
haftmann |
explicit constraints
|
changeset |
files
|
| Mon, 26 Jan 2009 22:14:51 +0100 |
haftmann |
entry point for Word library now named Word
|
changeset |
files
|
| Mon, 26 Jan 2009 22:14:19 +0100 |
haftmann |
fixed reading of class specs: declare class operations in context
|
changeset |
files
|
| Mon, 26 Jan 2009 22:14:18 +0100 |
haftmann |
stripped Id
|
changeset |
files
|
| Mon, 26 Jan 2009 22:14:17 +0100 |
haftmann |
streamlined definitions, executable equality
|
changeset |
files
|
| Mon, 26 Jan 2009 22:14:17 +0100 |
haftmann |
tuned header
|
changeset |
files
|
| Mon, 26 Jan 2009 22:14:16 +0100 |
haftmann |
entry point for Word library now named Word
|
changeset |
files
|
| Mon, 26 Jan 2009 08:23:55 +0100 |
haftmann |
correct proof of assm_intro rule
|
changeset |
files
|
| Mon, 26 Jan 2009 08:23:41 +0100 |
haftmann |
sorted_take, sorted_drop
|
changeset |
files
|
| Fri, 23 Jan 2009 19:52:02 +0100 |
haftmann |
merged
|
changeset |
files
|
| Fri, 23 Jan 2009 19:51:49 +0100 |
haftmann |
fixed fixme
|
changeset |
files
|
| Fri, 23 Jan 2009 19:51:49 +0100 |
haftmann |
avoiding misleading name duplicate
|
changeset |
files
|
| Fri, 23 Jan 2009 19:51:48 +0100 |
haftmann |
lemmas dom_const, dom_if
|
changeset |
files
|
| Fri, 23 Jan 2009 15:37:12 +0100 |
wenzelm |
merged
|
changeset |
files
|
| Fri, 23 Jan 2009 09:06:14 +0100 |
immler |
moved all output to watcher-thread
|
changeset |
files
|
| Fri, 23 Jan 2009 10:21:48 +0100 |
haftmann |
be more liberal with selected code statements
|
changeset |
files
|
| Fri, 23 Jan 2009 10:21:27 +0100 |
haftmann |
making SMLNJ happy
|
changeset |
files
|
| Thu, 22 Jan 2009 11:23:15 +0100 |
wenzelm |
tuned signature;
|
changeset |
files
|
| Thu, 22 Jan 2009 09:08:58 +0100 |
haftmann |
binding replaces Binding.T
|
changeset |
files
|