| Wed, 09 Nov 2011 17:57:42 +0100 |
wenzelm |
sort assignment before simultaneous term_check, not isolated parse_term;
|
file |
diff |
annotate
|
| Mon, 07 Nov 2011 22:22:01 +0100 |
blanchet |
avoid infinite recursion in peephole optimizer function -- this had a debilitating effect on rationals and reals
|
file |
diff |
annotate
|
| Mon, 07 Nov 2011 14:23:50 +0100 |
wenzelm |
clarified attribute "mono_set": pure declaration, proper export in ML;
|
file |
diff |
annotate
|
| 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
|