| Mon, 07 Nov 2011 14:14:20 +0100 |
wenzelm |
misc tuning;
|
file |
diff |
annotate
|
| Sat, 29 Oct 2011 12:57:43 +0200 |
wenzelm |
uniform treatment of syntax declaration wrt. aux. context (NB: notation avoids duplicate mixfix internally);
|
file |
diff |
annotate
|
| Fri, 28 Oct 2011 23:16:50 +0200 |
wenzelm |
refined Local_Theory.declaration {syntax = false, pervasive} semantics: update is applied to auxiliary context as well;
|
file |
diff |
annotate
|
| Fri, 21 Oct 2011 11:17:16 +0200 |
bulwahn |
NEWS
|
file |
diff |
annotate
|
| Wed, 19 Oct 2011 22:54:26 +0200 |
haftmann |
NEWS
|
file |
diff |
annotate
|
| Wed, 19 Oct 2011 15:42:43 +0200 |
wenzelm |
inlined @{thms} (ML compile-time) allows to get rid of legacy zadd_ac as well (cf. 49e305100097);
|
file |
diff |
annotate
|
| Wed, 19 Oct 2011 09:11:21 +0200 |
bulwahn |
NEWS
|
file |
diff |
annotate
|
| Mon, 17 Oct 2011 14:22:14 +0200 |
noschinl |
(old) NEWS
|
file |
diff |
annotate
|
| Fri, 14 Oct 2011 18:55:29 +0200 |
haftmann |
NEWS
|
file |
diff |
annotate
|
| Thu, 13 Oct 2011 11:45:33 +0200 |
wenzelm |
discontinued obsolete 'types' command;
|
file |
diff |
annotate
|
| Wed, 12 Oct 2011 16:21:07 +0200 |
wenzelm |
discontinued obsolete alias structure ProofContext;
|
file |
diff |
annotate
|
| Sun, 09 Oct 2011 11:13:53 +0200 |
huffman |
Int.thy: discontinued some legacy theorems
|
file |
diff |
annotate
|
| Mon, 26 Sep 2011 21:13:26 +0200 |
wenzelm |
back to post-release mode;
|
file |
diff |
annotate
|
| Mon, 26 Sep 2011 21:09:28 +0200 |
wenzelm |
tuned;
|
file |
diff |
annotate
|
| Mon, 26 Sep 2011 20:53:53 +0200 |
wenzelm |
misc tuning for release;
|
file |
diff |
annotate
|
| Thu, 22 Sep 2011 14:12:16 -0700 |
huffman |
discontinued legacy theorem names from RealDef.thy
|
file |
diff |
annotate
|
| Thu, 22 Sep 2011 12:55:19 -0700 |
huffman |
discontinued HOLCF legacy theorem names
|
file |
diff |
annotate
|
| Thu, 22 Sep 2011 10:02:16 -0400 |
hoelzl |
NEWS: mention replacement lemmas for the removed ones in Complete_Lattices
|
file |
diff |
annotate
|
| Wed, 21 Sep 2011 00:12:36 +0200 |
nipkow |
merged
|
file |
diff |
annotate
|
| Tue, 20 Sep 2011 05:47:11 +0200 |
nipkow |
New proof method "induction" that gives induction hypotheses the name IH.
|
file |
diff |
annotate
|
| Tue, 20 Sep 2011 22:11:22 +0200 |
haftmann |
official status for UN_singleton
|
file |
diff |
annotate
|
| Sun, 18 Sep 2011 15:57:36 +0200 |
wenzelm |
tuned;
|
file |
diff |
annotate
|
| Sun, 18 Sep 2011 15:39:55 +0200 |
wenzelm |
separated NEWS for Isabelle2011 from Isabelle2011-1 (cf. e1139e612b55);
|
file |
diff |
annotate
|
| Sun, 18 Sep 2011 14:48:25 +0200 |
wenzelm |
some tuning and re-ordering for release;
|
file |
diff |
annotate
|
| Sun, 18 Sep 2011 14:34:24 +0200 |
wenzelm |
misc tuning for release;
|
file |
diff |
annotate
|
| Thu, 15 Sep 2011 12:40:08 -0400 |
hoelzl |
removed further legacy rules from Complete_Lattices
|
file |
diff |
annotate
|
| Thu, 15 Sep 2011 17:06:00 +0200 |
noschinl |
NEWS on Complete_Lattices, Lattices
|
file |
diff |
annotate
|
| Tue, 13 Sep 2011 09:56:38 +0200 |
bulwahn |
correcting NEWS
|
file |
diff |
annotate
|
| Mon, 12 Sep 2011 13:19:10 -0700 |
huffman |
NEWS and CONTRIBUTORS
|
file |
diff |
annotate
|
| Mon, 12 Sep 2011 11:54:20 -0700 |
huffman |
remove redundant lemma Lim_sequentially in favor of lemma LIMSEQ_def
|
file |
diff |
annotate
|
| Mon, 12 Sep 2011 10:28:45 -0700 |
huffman |
fix typos
|
file |
diff |
annotate
|
| Mon, 12 Sep 2011 09:37:49 -0700 |
huffman |
NEWS for euclidean_space class
|
file |
diff |
annotate
|
| Mon, 12 Sep 2011 09:57:33 -0400 |
hoelzl |
adding NEWS and CONTRIBUTORS
|
file |
diff |
annotate
|
| Mon, 12 Sep 2011 13:35:35 +0200 |
bulwahn |
merged
|
file |
diff |
annotate
|
| Mon, 12 Sep 2011 10:27:36 +0200 |
bulwahn |
adding NEWS and CONTRIBUTORS
|
file |
diff |
annotate
|
| Mon, 12 Sep 2011 09:45:53 +0200 |
bulwahn |
tuned some symbol that probably went there by some strange encoding issue
|
file |
diff |
annotate
|
| Mon, 12 Sep 2011 11:05:32 +0200 |
blanchet |
added my contributions to NEWS and CONTRIBUTORS
|
file |
diff |
annotate
|
| Mon, 12 Sep 2011 09:07:23 +0200 |
nipkow |
NEWS fastsimp -> fastforce
|
file |
diff |
annotate
|
| Sun, 11 Sep 2011 13:49:42 -0700 |
huffman |
NEWS for Library/Product_Lattice.thy
|
file |
diff |
annotate
|
| Fri, 09 Sep 2011 00:22:18 +0200 |
krauss |
added syntactic classes for "inf" and "sup"
|
file |
diff |
annotate
|
| Wed, 07 Sep 2011 19:24:28 -0700 |
huffman |
merged
|
file |
diff |
annotate
|
| Wed, 07 Sep 2011 09:45:39 -0700 |
huffman |
remove duplicate lemma real_of_int_real_of_nat in favor of real_of_int_of_nat_eq
|
file |
diff |
annotate
|
| Thu, 08 Sep 2011 00:23:23 +0200 |
wenzelm |
merged
|
file |
diff |
annotate
|
| Wed, 07 Sep 2011 23:38:52 +0200 |
haftmann |
theory of saturated naturals contributed by Peter Gammie
|
file |
diff |
annotate
|
| Wed, 07 Sep 2011 21:10:47 +0200 |
wenzelm |
NEWS on IsabelleText font;
|
file |
diff |
annotate
|
| Wed, 07 Sep 2011 20:49:45 +0200 |
wenzelm |
some updates for release;
|
file |
diff |
annotate
|
| Wed, 07 Sep 2011 20:29:54 +0200 |
wenzelm |
some tuning for release;
|
file |
diff |
annotate
|
| Wed, 07 Sep 2011 11:26:27 +0200 |
wenzelm |
more NEWS;
|
file |
diff |
annotate
|
| Tue, 06 Sep 2011 21:56:11 +0200 |
wenzelm |
some Isabelle/jEdit NEWS;
|
file |
diff |
annotate
|
| Tue, 06 Sep 2011 07:48:59 -0700 |
huffman |
remove redundant lemma real_sum_squared_expand in favor of power2_sum
|
file |
diff |
annotate
|
| Tue, 06 Sep 2011 07:45:18 -0700 |
huffman |
remove redundant lemma LIMSEQ_Complex in favor of tendsto_Complex
|
file |
diff |
annotate
|
| Sun, 04 Sep 2011 10:05:52 -0700 |
huffman |
remove redundant lemmas expi_add and expi_zero
|
file |
diff |
annotate
|
| Sun, 04 Sep 2011 09:49:45 -0700 |
huffman |
remove redundant lemmas about LIMSEQ
|
file |
diff |
annotate
|
| Sat, 03 Sep 2011 09:26:11 -0700 |
huffman |
remove duplicate lemma finite_choice in favor of finite_set_choice
|
file |
diff |
annotate
|
| Fri, 02 Sep 2011 16:48:30 -0700 |
huffman |
remove redundant lemma reals_complete2 in favor of complete_real
|
file |
diff |
annotate
|
| Fri, 02 Sep 2011 13:57:12 -0700 |
huffman |
remove more duplicate lemmas
|
file |
diff |
annotate
|
| Thu, 01 Sep 2011 10:41:19 -0700 |
huffman |
simplify some proofs about uniform continuity, and add some new ones;
|
file |
diff |
annotate
|
| Thu, 01 Sep 2011 09:02:14 -0700 |
huffman |
modernize lemmas about 'continuous' and 'continuous_on';
|
file |
diff |
annotate
|
| Sun, 28 Aug 2011 09:20:12 -0700 |
huffman |
discontinue many legacy theorems about LIM and LIMSEQ, in favor of tendsto theorems
|
file |
diff |
annotate
|
| Fri, 26 Aug 2011 15:11:26 -0700 |
huffman |
NEWS entry for setsum_norm ~> norm_setsum
|
file |
diff |
annotate
|