| Tue, 11 Jan 2011 19:55:34 +0100 |
wenzelm |
isabelle version -i;
|
changeset |
files
|
| Tue, 11 Jan 2011 18:23:29 +0100 |
haftmann |
NEWS
|
changeset |
files
|
| Tue, 11 Jan 2011 17:59:35 +0100 |
bulwahn |
NEWS
|
changeset |
files
|
| Tue, 11 Jan 2011 17:38:03 +0100 |
krauss |
eliminated duplication
|
changeset |
files
|
| Tue, 11 Jan 2011 17:00:21 +0100 |
wenzelm |
merged
|
changeset |
files
|
| Tue, 11 Jan 2011 14:14:13 +0100 |
haftmann |
tuned text
|
changeset |
files
|
| Tue, 11 Jan 2011 14:12:37 +0100 |
haftmann |
"enriched_type" replaces less specific "type_lifting"
|
changeset |
files
|
| Tue, 11 Jan 2011 16:23:28 +0100 |
wenzelm |
clarified notion Position.is_reported;
|
changeset |
files
|
| Mon, 10 Jan 2011 22:03:24 +0100 |
wenzelm |
refined report_parse_tree: reverse reports happen to produce proper type information for inlined @{term}, @{typ} etc.;
|
changeset |
files
|
| Mon, 10 Jan 2011 21:45:44 +0100 |
wenzelm |
refined ML_Lex.flatten: ensure proper separation of tokens;
|
changeset |
files
|
| Mon, 10 Jan 2011 21:21:23 +0100 |
wenzelm |
ML compiler: more careful treatment of input tokens -- trailing space ensures proper separation and end position (cf. 82c1e348bc18, 08240feb69c7);
|
changeset |
files
|
| Mon, 10 Jan 2011 18:59:02 +0100 |
boehmes |
use just one data slot to VC-related information
|
changeset |
files
|
| Mon, 10 Jan 2011 18:58:54 +0100 |
boehmes |
be more precise: also merge option values
|
changeset |
files
|
| Mon, 10 Jan 2011 17:41:45 +0100 |
boehmes |
only print warning in a visible context (previously, the warning was printed more than once)
|
changeset |
files
|
| Mon, 10 Jan 2011 17:39:54 +0100 |
boehmes |
dropped superfluous error message
|
changeset |
files
|
| Mon, 10 Jan 2011 17:37:11 +0100 |
krauss |
removed obsolete make target (now in doc-src, cf. 28b487cd9e15)
|
changeset |
files
|