chaieb [Wed, 28 Jan 2009 13:23:59 +0000] rev 29674
Added theorems setsum_reindex_nonzero, setsum_mono_zero_left, setsum_mono_zero_right, setsum_mono_zero_cong_left, setsum_mono_zero_cong_right, setsum_delta, strong_setprod_reindex_cong, setprod_delta
nipkow [Thu, 29 Jan 2009 10:08:25 +0100] rev 29673
merged
nipkow [Thu, 29 Jan 2009 10:07:43 +0100] rev 29672
commented out unused lemmas. May need to be put back by Brian.
nipkow [Wed, 28 Jan 2009 21:49:25 +0100] rev 29671
-
nipkow [Wed, 28 Jan 2009 17:12:25 +0100] rev 29670
removed spurious conflic msg
nipkow [Wed, 28 Jan 2009 16:57:36 +0100] rev 29669
merged
nipkow [Wed, 28 Jan 2009 16:57:12 +0100] rev 29668
merged - resolving conflics
nipkow [Wed, 28 Jan 2009 16:29:16 +0100] rev 29667
Replaced group_ and ring_simps by algebra_simps;
removed compare_rls - use algebra_simps now
haftmann [Wed, 28 Jan 2009 16:35:57 +0100] rev 29666
merged
haftmann [Wed, 28 Jan 2009 16:35:42 +0100] rev 29665
explicit check for exactly one type variable in class specification elements
huffman [Wed, 28 Jan 2009 06:03:46 -0800] rev 29664
merged
huffman [Tue, 27 Jan 2009 22:39:41 -0800] rev 29663
merged
huffman [Thu, 22 Jan 2009 06:42:05 -0800] rev 29662
removed use of prev_cont_thms reference
huffman [Thu, 22 Jan 2009 06:09:41 -0800] rev 29661
merged
huffman [Wed, 21 Jan 2009 21:01:15 -0800] rev 29660
add lemmas about div/mod with multiplication
huffman [Wed, 21 Jan 2009 20:20:56 -0800] rev 29659
add lemmas about smult
haftmann [Wed, 28 Jan 2009 13:36:24 +0100] rev 29658
merged
haftmann [Wed, 28 Jan 2009 13:36:11 +0100] rev 29657
slightly adapted towards more uniformity with div/mod on nat
haftmann [Wed, 28 Jan 2009 11:04:45 +0100] rev 29656
merged
haftmann [Wed, 28 Jan 2009 11:03:42 +0100] rev 29655
Plain, Main form meeting points in import hierarchy
haftmann [Wed, 28 Jan 2009 11:03:16 +0100] rev 29654
Plain, Main form meeting points in import hierarchy
haftmann [Wed, 28 Jan 2009 11:02:12 +0100] rev 29653
added lemma abs_sng
haftmann [Wed, 28 Jan 2009 11:02:12 +0100] rev 29652
nat is a bot instance
haftmann [Wed, 28 Jan 2009 11:02:11 +0100] rev 29651
slightly adapted towards more uniformity with div/mod on nat
haftmann [Wed, 28 Jan 2009 11:04:10 +0100] rev 29650
Reflection.thy now in HOL/Library
wenzelm [Wed, 28 Jan 2009 11:36:45 +0100] rev 29649
more robust treatment of SwingUtilities.isEventDispatchThread;
wenzelm [Wed, 28 Jan 2009 10:43:31 +0100] rev 29648
annotate shared vars as @volatile;
wenzelm [Tue, 27 Jan 2009 19:56:26 +0100] rev 29647
updated generated file;
wenzelm [Tue, 27 Jan 2009 19:56:20 +0100] rev 29646
added label;
wenzelm [Tue, 27 Jan 2009 15:47:22 +0100] rev 29645
plain non-dependent types;
wenzelm [Tue, 27 Jan 2009 15:22:46 +0100] rev 29644
turned IsarDocument into trait for IsabelleProcess;
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;
wenzelm [Tue, 27 Jan 2009 14:28:51 +0100] rev 29642
thm_proof: recovered single-threaded version;
wenzelm [Tue, 27 Jan 2009 13:52:32 +0100] rev 29641
merged
wenzelm [Tue, 27 Jan 2009 13:41:45 +0100] rev 29640
recovered example types from WordMain.thy;
wenzelm [Tue, 27 Jan 2009 12:59:38 +0100] rev 29639
merged
wenzelm [Tue, 27 Jan 2009 12:59:22 +0100] rev 29638
added share_common_data -- reduces heap space, but takes long;
wenzelm [Tue, 27 Jan 2009 12:57:24 +0100] rev 29637
use https;
wenzelm [Tue, 27 Jan 2009 00:42:12 +0100] rev 29636
thm_proof: replaced lazy by composed futures;
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;
haftmann [Mon, 26 Jan 2009 22:15:35 +0100] rev 29634
explicit constraints
haftmann [Mon, 26 Jan 2009 22:14:51 +0100] rev 29633
entry point for Word library now named Word
haftmann [Mon, 26 Jan 2009 22:14:19 +0100] rev 29632
fixed reading of class specs: declare class operations in context
haftmann [Mon, 26 Jan 2009 22:14:18 +0100] rev 29631
stripped Id
haftmann [Mon, 26 Jan 2009 22:14:17 +0100] rev 29630
streamlined definitions, executable equality
haftmann [Mon, 26 Jan 2009 22:14:17 +0100] rev 29629
tuned header
haftmann [Mon, 26 Jan 2009 22:14:16 +0100] rev 29628
entry point for Word library now named Word
haftmann [Mon, 26 Jan 2009 08:23:55 +0100] rev 29627
correct proof of assm_intro rule
haftmann [Mon, 26 Jan 2009 08:23:41 +0100] rev 29626
sorted_take, sorted_drop
haftmann [Fri, 23 Jan 2009 19:52:02 +0100] rev 29625
merged
haftmann [Fri, 23 Jan 2009 19:51:49 +0100] rev 29624
fixed fixme
haftmann [Fri, 23 Jan 2009 19:51:49 +0100] rev 29623
avoiding misleading name duplicate
haftmann [Fri, 23 Jan 2009 19:51:48 +0100] rev 29622
lemmas dom_const, dom_if
wenzelm [Fri, 23 Jan 2009 15:37:12 +0100] rev 29621
merged
immler@in.tum.de [Fri, 23 Jan 2009 09:06:14 +0100] rev 29620
moved all output to watcher-thread
haftmann [Fri, 23 Jan 2009 10:21:48 +0100] rev 29619
be more liberal with selected code statements
haftmann [Fri, 23 Jan 2009 10:21:27 +0100] rev 29618
making SMLNJ happy
wenzelm [Thu, 22 Jan 2009 11:23:15 +0100] rev 29617
tuned signature;
haftmann [Thu, 22 Jan 2009 09:08:58 +0100] rev 29616
binding replaces Binding.T
haftmann [Thu, 22 Jan 2009 09:04:56 +0100] rev 29615
binding replaces bstring