Tue, 27 Jan 2009 19:56:26 +0100 updated generated file;
wenzelm [Tue, 27 Jan 2009 19:56:26 +0100] rev 29647
updated generated file;
Tue, 27 Jan 2009 19:56:20 +0100 added label;
wenzelm [Tue, 27 Jan 2009 19:56:20 +0100] rev 29646
added label;
Tue, 27 Jan 2009 15:47:22 +0100 plain non-dependent types;
wenzelm [Tue, 27 Jan 2009 15:47:22 +0100] rev 29645
plain non-dependent types;
Tue, 27 Jan 2009 15:22:46 +0100 turned IsarDocument into trait for IsabelleProcess;
wenzelm [Tue, 27 Jan 2009 15:22:46 +0100] rev 29644
turned IsarDocument into trait for IsabelleProcess;
Tue, 27 Jan 2009 14:45:52 +0100 HOL_USEDIR_OPTIONS: -Q false, giving up parallel proofs for now due to memory shortage;
wenzelm [Tue, 27 Jan 2009 14:45:52 +0100] rev 29643
HOL_USEDIR_OPTIONS: -Q false, giving up parallel proofs for now due to memory shortage;
Tue, 27 Jan 2009 14:28:51 +0100 thm_proof: recovered single-threaded version;
wenzelm [Tue, 27 Jan 2009 14:28:51 +0100] rev 29642
thm_proof: recovered single-threaded version;
Tue, 27 Jan 2009 13:52:32 +0100 merged
wenzelm [Tue, 27 Jan 2009 13:52:32 +0100] rev 29641
merged
Tue, 27 Jan 2009 13:41:45 +0100 recovered example types from WordMain.thy;
wenzelm [Tue, 27 Jan 2009 13:41:45 +0100] rev 29640
recovered example types from WordMain.thy;
Tue, 27 Jan 2009 12:59:38 +0100 merged
wenzelm [Tue, 27 Jan 2009 12:59:38 +0100] rev 29639
merged
Tue, 27 Jan 2009 12:59:22 +0100 added share_common_data -- reduces heap space, but takes long;
wenzelm [Tue, 27 Jan 2009 12:59:22 +0100] rev 29638
added share_common_data -- reduces heap space, but takes long;
Tue, 27 Jan 2009 12:57:24 +0100 use https;
wenzelm [Tue, 27 Jan 2009 12:57:24 +0100] rev 29637
use https;
Tue, 27 Jan 2009 00:42:12 +0100 thm_proof: replaced lazy by composed futures;
wenzelm [Tue, 27 Jan 2009 00:42:12 +0100] rev 29636
thm_proof: replaced lazy by composed futures;
Tue, 27 Jan 2009 00:29:37 +0100 proof_body: turned lazy into future -- ensures that body is fulfilled eventually, without explicit force;
wenzelm [Tue, 27 Jan 2009 00:29:37 +0100] rev 29635
proof_body: turned lazy into future -- ensures that body is fulfilled eventually, without explicit force;
Mon, 26 Jan 2009 22:15:35 +0100 explicit constraints
haftmann [Mon, 26 Jan 2009 22:15:35 +0100] rev 29634
explicit constraints
Mon, 26 Jan 2009 22:14:51 +0100 entry point for Word library now named Word
haftmann [Mon, 26 Jan 2009 22:14:51 +0100] rev 29633
entry point for Word library now named Word
Mon, 26 Jan 2009 22:14:19 +0100 fixed reading of class specs: declare class operations in context
haftmann [Mon, 26 Jan 2009 22:14:19 +0100] rev 29632
fixed reading of class specs: declare class operations in context
Mon, 26 Jan 2009 22:14:18 +0100 stripped Id
haftmann [Mon, 26 Jan 2009 22:14:18 +0100] rev 29631
stripped Id
Mon, 26 Jan 2009 22:14:17 +0100 streamlined definitions, executable equality
haftmann [Mon, 26 Jan 2009 22:14:17 +0100] rev 29630
streamlined definitions, executable equality
Mon, 26 Jan 2009 22:14:17 +0100 tuned header
haftmann [Mon, 26 Jan 2009 22:14:17 +0100] rev 29629
tuned header
Mon, 26 Jan 2009 22:14:16 +0100 entry point for Word library now named Word
haftmann [Mon, 26 Jan 2009 22:14:16 +0100] rev 29628
entry point for Word library now named Word
Mon, 26 Jan 2009 08:23:55 +0100 correct proof of assm_intro rule
haftmann [Mon, 26 Jan 2009 08:23:55 +0100] rev 29627
correct proof of assm_intro rule
Mon, 26 Jan 2009 08:23:41 +0100 sorted_take, sorted_drop
haftmann [Mon, 26 Jan 2009 08:23:41 +0100] rev 29626
sorted_take, sorted_drop
Fri, 23 Jan 2009 19:52:02 +0100 merged
haftmann [Fri, 23 Jan 2009 19:52:02 +0100] rev 29625
merged
Fri, 23 Jan 2009 19:51:49 +0100 fixed fixme
haftmann [Fri, 23 Jan 2009 19:51:49 +0100] rev 29624
fixed fixme
Fri, 23 Jan 2009 19:51:49 +0100 avoiding misleading name duplicate
haftmann [Fri, 23 Jan 2009 19:51:49 +0100] rev 29623
avoiding misleading name duplicate
Fri, 23 Jan 2009 19:51:48 +0100 lemmas dom_const, dom_if
haftmann [Fri, 23 Jan 2009 19:51:48 +0100] rev 29622
lemmas dom_const, dom_if
Fri, 23 Jan 2009 15:37:12 +0100 merged
wenzelm [Fri, 23 Jan 2009 15:37:12 +0100] rev 29621
merged
Fri, 23 Jan 2009 09:06:14 +0100 moved all output to watcher-thread
immler@in.tum.de [Fri, 23 Jan 2009 09:06:14 +0100] rev 29620
moved all output to watcher-thread
Fri, 23 Jan 2009 10:21:48 +0100 be more liberal with selected code statements
haftmann [Fri, 23 Jan 2009 10:21:48 +0100] rev 29619
be more liberal with selected code statements
Fri, 23 Jan 2009 10:21:27 +0100 making SMLNJ happy
haftmann [Fri, 23 Jan 2009 10:21:27 +0100] rev 29618
making SMLNJ happy
Thu, 22 Jan 2009 11:23:15 +0100 tuned signature;
wenzelm [Thu, 22 Jan 2009 11:23:15 +0100] rev 29617
tuned signature;
Thu, 22 Jan 2009 09:08:58 +0100 binding replaces Binding.T
haftmann [Thu, 22 Jan 2009 09:08:58 +0100] rev 29616
binding replaces Binding.T
(0) -10000 -3000 -1000 -300 -100 -50 -32 +32 +50 +100 +300 +1000 +3000 +10000 +30000 tip