| Fri, 24 Sep 2010 16:17:59 +0200 |
wenzelm |
clarified @{type} antiquotation: abbreviations and nonterminals count as "syntactic", disallow TFrees;
|
file |
diff |
annotate
|
| Thu, 23 Sep 2010 09:53:52 +0200 |
haftmann |
CONTRIBUTORS and NEWS
|
file |
diff |
annotate
|
| Wed, 22 Sep 2010 18:21:48 +0200 |
wenzelm |
renamed setmp_noncritical to Unsynchronized.setmp to emphasize its meaning;
|
file |
diff |
annotate
|
| Mon, 20 Sep 2010 16:05:25 +0200 |
wenzelm |
renamed structure PureThy to Pure_Thy and moved most content to Global_Theory, to emphasize that this is global-only;
|
file |
diff |
annotate
|
| Fri, 17 Sep 2010 22:17:57 +0200 |
wenzelm |
discontinued Output.debug, which belongs to early PGIP experiments (b6788dbd2ef9) and causes just too many problems (like spamming the message channel if it is used by more than one module);
|
file |
diff |
annotate
|
| Mon, 13 Sep 2010 14:55:21 +0200 |
haftmann |
merged
|
file |
diff |
annotate
|
| Mon, 13 Sep 2010 14:53:56 +0200 |
haftmann |
'class' and 'type' are now antiquoations by default
|
file |
diff |
annotate
|
| Mon, 13 Sep 2010 11:13:15 +0200 |
nipkow |
renamed lemmas: ext_iff -> fun_eq_iff, set_ext_iff -> set_eq_iff, set_ext -> set_eqI
|
file |
diff |
annotate
|
| Mon, 13 Sep 2010 08:43:48 +0200 |
nipkow |
added and renamed lemmas
|
file |
diff |
annotate
|
| Fri, 10 Sep 2010 15:17:44 +0200 |
wenzelm |
merged
|
file |
diff |
annotate
|
| Thu, 09 Sep 2010 14:38:14 +0200 |
bulwahn |
changing String.literal to a type instead of a datatype
|
file |
diff |
annotate
|
| Thu, 09 Sep 2010 18:32:21 +0200 |
wenzelm |
NEWS: some notes on interrupts;
|
file |
diff |
annotate
|
| Wed, 08 Sep 2010 13:25:22 +0200 |
haftmann |
NEWS
|
file |
diff |
annotate
|
| Tue, 07 Sep 2010 12:04:18 +0200 |
nipkow |
renamed expand_*_eq in HOLCF as well
|
file |
diff |
annotate
|
| Mon, 06 Sep 2010 22:08:49 +0200 |
wenzelm |
ML_Context.thm and ML_Context.thms no longer pervasive;
|
file |
diff |
annotate
|
| Mon, 06 Sep 2010 12:38:45 +0200 |
wenzelm |
merged;
|
file |
diff |
annotate
|
| Sun, 05 Sep 2010 21:39:24 +0200 |
krauss |
removed duplicate lemma
|
file |
diff |
annotate
|
| Sun, 05 Sep 2010 23:16:21 +0200 |
wenzelm |
turned show_brackets into proper configuration option;
|
file |
diff |
annotate
|
| Sun, 05 Sep 2010 21:41:24 +0200 |
wenzelm |
turned show_sorts/show_types into proper configuration options;
|
file |
diff |
annotate
|
| Fri, 03 Sep 2010 23:54:48 +0200 |
wenzelm |
turned eta_contract into proper configuration option;
|
file |
diff |
annotate
|
| Fri, 03 Sep 2010 22:36:16 +0200 |
wenzelm |
configuration options Syntax.ambiguity_enabled (inverse of former Syntax.ambiguity_is_error), Syntax.ambiguity_level (with Isar attribute "syntax_ambiguity_level"), Syntax.ambiguity_limit;
|
file |
diff |
annotate
|
| Fri, 03 Sep 2010 21:13:53 +0200 |
wenzelm |
pretty_goals: turned some global references and function arguments into configuration options (goals_limit = 10, goals_total = true, show_main_goal = false) depending on the context;
|
file |
diff |
annotate
|
| Fri, 03 Sep 2010 12:01:47 +0200 |
wenzelm |
merged
|
file |
diff |
annotate
|
| Thu, 02 Sep 2010 18:45:23 +0200 |
hoelzl |
merged
|
file |
diff |
annotate
|
| Thu, 02 Sep 2010 13:32:17 +0200 |
hoelzl |
NEWS
|
file |
diff |
annotate
|
| Fri, 03 Sep 2010 11:21:58 +0200 |
wenzelm |
turned show_consts into proper configuration option;
|
file |
diff |
annotate
|
| Thu, 02 Sep 2010 00:48:07 +0200 |
wenzelm |
turned show_question_marks into proper configuration option;
|
file |
diff |
annotate
|
| Sat, 28 Aug 2010 16:14:32 +0200 |
haftmann |
formerly unnamed infix equality now named HOL.eq
|
file |
diff |
annotate
|
| Sat, 28 Aug 2010 11:42:33 +0200 |
haftmann |
merged
|
file |
diff |
annotate
|
| Fri, 27 Aug 2010 19:34:23 +0200 |
haftmann |
renamed class/constant eq to equal; tuned some instantiations
|
file |
diff |
annotate
|