Wed, 12 May 2010 11:13:33 +0200 hoelzl clarified NEWS entry
Wed, 12 May 2010 11:08:15 +0200 hoelzl merged
Wed, 12 May 2010 11:07:46 +0200 hoelzl added NEWS entry
Tue, 11 May 2010 19:19:45 +0200 hoelzl Added atLeastAtMost_singleton_iff, atLeastAtMost_singleton'
Tue, 11 May 2010 19:21:39 +0200 hoelzl Add rules directly to the corresponding class locales instead.
Tue, 11 May 2010 19:21:05 +0200 hoelzl Removed usage of normalizating locales.
Tue, 11 May 2010 21:55:41 -0700 huffman speed up some proofs, fixing linarith_split_limit warnings
Tue, 11 May 2010 19:38:16 -0700 huffman fix some linarith_split_limit warnings
Tue, 11 May 2010 19:01:35 -0700 huffman include iszero_simps in semiring_norm just once (they are already included in rel_simps)
Tue, 11 May 2010 19:00:32 -0700 huffman fix duplicate simp rule warning
Tue, 11 May 2010 18:06:58 -0700 huffman no more RealPow.thy (remaining lemmas moved to RealDef.thy)
Tue, 11 May 2010 17:20:11 -0700 huffman merged
Tue, 11 May 2010 12:38:07 -0700 huffman simplify code for emptiness check
Tue, 11 May 2010 12:05:19 -0700 huffman removed lemma real_sq_order; use power2_le_imp_le instead
Tue, 11 May 2010 21:27:09 +0200 haftmann merged
Tue, 11 May 2010 19:06:18 +0200 haftmann merged
Tue, 11 May 2010 19:00:16 +0200 haftmann represent de-Bruin indices simply by position in list
Tue, 11 May 2010 18:46:03 +0200 haftmann tuned reification functions
Tue, 11 May 2010 18:31:36 +0200 haftmann tuned code; toward a tightended interface with generated code
Tue, 11 May 2010 11:58:34 -0700 huffman fix spelling of 'superseded'
Tue, 11 May 2010 11:57:14 -0700 huffman NEWS: removed theory PReal
Tue, 11 May 2010 11:40:39 -0700 huffman collected NEWS updates for HOLCF
Tue, 11 May 2010 11:02:56 -0700 huffman merged
Tue, 11 May 2010 09:10:31 -0700 huffman move floor lemmas from RealPow.thy to RComplete.thy
Tue, 11 May 2010 07:58:48 -0700 huffman add lemma tendsto_Complex
Tue, 11 May 2010 06:30:48 -0700 huffman move some theorems from RealPow.thy to Transcendental.thy
Tue, 11 May 2010 06:27:06 -0700 huffman add lemma power2_eq_1_iff; generalize some other lemmas
Mon, 10 May 2010 21:33:48 -0700 huffman minimize imports
Mon, 10 May 2010 21:27:52 -0700 huffman move lemma real_mult_is_one to Rings.thy, renamed to square_eq_1_iff
Wed, 12 May 2010 12:50:00 +0200 wenzelm clarified Pretty.font_metrics;
Wed, 12 May 2010 11:31:05 +0200 wenzelm format as topmost list of "divs", not just adjacent "spans" -- for proper line breaking;
Wed, 12 May 2010 11:28:52 +0200 wenzelm tuned;
Tue, 11 May 2010 23:36:06 +0200 wenzelm more precise pretty printing based on actual font metrics;
Tue, 11 May 2010 23:09:49 +0200 wenzelm predefined spaces;
Tue, 11 May 2010 17:55:19 +0200 wenzelm merged
Tue, 11 May 2010 15:47:31 +0200 wenzelm support Isabelle plugin properties with defaults;
Tue, 11 May 2010 08:52:22 +0100 Christian Urban merged
Tue, 11 May 2010 07:45:47 +0100 Christian Urban tuned proof so that no simplifier warning is printed
Tue, 11 May 2010 08:36:02 +0200 haftmann renamed former Int.int_induct to Int.int_of_nat_induct, former Presburger.int_induct to Int.int_induct: is more conservative and more natural than the intermediate solution
Tue, 11 May 2010 08:30:02 +0200 haftmann merged
Tue, 11 May 2010 08:29:42 +0200 haftmann tuned
Tue, 11 May 2010 08:29:42 +0200 haftmann theorem Presburger.int_induct has been renamed to Int.int_bidirectional_induct
Mon, 10 May 2010 15:33:32 +0200 haftmann tuned; dropped strange myassoc2
Mon, 10 May 2010 15:24:43 +0200 haftmann stylized COOPER exception
Mon, 10 May 2010 15:21:13 +0200 haftmann simplified oracle
Mon, 10 May 2010 15:00:53 +0200 haftmann shorten names
Mon, 10 May 2010 14:57:04 +0200 haftmann updated references to ML files
Mon, 10 May 2010 14:55:06 +0200 haftmann only one module fpr presburger method
Mon, 10 May 2010 14:55:04 +0200 haftmann moved int induction lemma to theory Int as int_bidirectional_induct
Mon, 10 May 2010 14:18:41 +0200 haftmann tuned theory text; dropped unused lemma
Mon, 10 May 2010 14:11:50 +0200 haftmann one structure is better than three
Mon, 10 May 2010 13:58:18 +0200 haftmann less complex organization of cooper source code
Mon, 10 May 2010 12:25:49 +0200 haftmann dropped unused bindings; avoid open (documents dependency on generated code more explicitly)
Mon, 10 May 2010 14:53:33 -0700 huffman add real_mult_commute to legacy theorem names
Mon, 10 May 2010 12:12:58 -0700 huffman new construction of real numbers using Cauchy sequences
Mon, 10 May 2010 11:47:56 -0700 huffman add more credits to ex/Dedekind_Real.thy
Mon, 10 May 2010 11:30:05 -0700 huffman put construction of reals using Dedekind cuts in HOL/ex
Tue, 11 May 2010 10:36:50 +0200 wenzelm disable two stage save by default, to avoid change of file permissions (notably the dreaded executable bit on Cygwin);
Mon, 10 May 2010 23:46:49 +0200 wenzelm simple dialogs: ensure Swing thread;
Mon, 10 May 2010 23:36:47 +0200 wenzelm font size re-adjustment according to Lobo internals;
(0) -30000 -10000 -3000 -1000 -300 -100 -60 +60 +100 +300 +1000 +3000 +10000 +30000 tip