Wed, 28 Jan 2009 13:36:11 +0100 |
haftmann |
slightly adapted towards more uniformity with div/mod on nat
|
changeset |
files
|
Wed, 28 Jan 2009 11:04:45 +0100 |
haftmann |
merged
|
changeset |
files
|
Wed, 28 Jan 2009 11:03:42 +0100 |
haftmann |
Plain, Main form meeting points in import hierarchy
|
changeset |
files
|
Wed, 28 Jan 2009 11:03:16 +0100 |
haftmann |
Plain, Main form meeting points in import hierarchy
|
changeset |
files
|
Wed, 28 Jan 2009 11:02:12 +0100 |
haftmann |
added lemma abs_sng
|
changeset |
files
|
Wed, 28 Jan 2009 11:02:12 +0100 |
haftmann |
nat is a bot instance
|
changeset |
files
|
Wed, 28 Jan 2009 11:02:11 +0100 |
haftmann |
slightly adapted towards more uniformity with div/mod on nat
|
changeset |
files
|
Wed, 28 Jan 2009 11:04:10 +0100 |
haftmann |
Reflection.thy now in HOL/Library
|
changeset |
files
|
Wed, 28 Jan 2009 11:36:45 +0100 |
wenzelm |
more robust treatment of SwingUtilities.isEventDispatchThread;
|
changeset |
files
|
Wed, 28 Jan 2009 10:43:31 +0100 |
wenzelm |
annotate shared vars as @volatile;
|
changeset |
files
|
Tue, 27 Jan 2009 19:56:26 +0100 |
wenzelm |
updated generated file;
|
changeset |
files
|
Tue, 27 Jan 2009 19:56:20 +0100 |
wenzelm |
added label;
|
changeset |
files
|
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
|
Thu, 22 Jan 2009 09:04:56 +0100 |
haftmann |
binding replaces bstring
|
changeset |
files
|
Thu, 22 Jan 2009 09:04:46 +0100 |
haftmann |
simplified handling of base sort, dropped axclass
|
changeset |
files
|
Thu, 22 Jan 2009 09:04:45 +0100 |
haftmann |
dropped print_interps
|
changeset |
files
|
Thu, 22 Jan 2009 09:04:45 +0100 |
haftmann |
binding replaces bstring
|
changeset |
files
|
Wed, 21 Jan 2009 23:42:37 +0100 |
haftmann |
merged
|
changeset |
files
|
Wed, 21 Jan 2009 23:40:23 +0100 |
haftmann |
allow empty class specs
|
changeset |
files
|
Wed, 21 Jan 2009 23:40:23 +0100 |
haftmann |
changed import hierarchy
|
changeset |
files
|
Wed, 21 Jan 2009 23:40:23 +0100 |
haftmann |
no base sort in class import
|
changeset |
files
|
Wed, 21 Jan 2009 23:25:17 +0100 |
wenzelm |
updated generated files;
|
changeset |
files
|
Wed, 21 Jan 2009 23:21:44 +0100 |
wenzelm |
removed Ids;
|
changeset |
files
|
Wed, 21 Jan 2009 22:26:49 +0100 |
wenzelm |
eliminated obsolete var morphism;
|
changeset |
files
|
Wed, 21 Jan 2009 22:26:49 +0100 |
wenzelm |
eliminated obsolete var morphism;
|
changeset |
files
|
Wed, 21 Jan 2009 22:26:48 +0100 |
wenzelm |
eliminated obsolete var morphism;
|
changeset |
files
|
Wed, 21 Jan 2009 20:24:44 +0100 |
wenzelm |
merged
|
changeset |
files
|
Wed, 21 Jan 2009 20:20:43 +0100 |
wenzelm |
tuned whitespace;
|
changeset |
files
|
Wed, 21 Jan 2009 20:05:31 +0100 |
wenzelm |
merged
|
changeset |
files
|
Wed, 21 Jan 2009 15:26:02 +0100 |
immler |
removed vampire-wrapper (remote-script covers that)
|
changeset |
files
|
Wed, 21 Jan 2009 15:22:51 +0100 |
immler |
2 provers
|
changeset |
files
|