2007-10-22 clarified Haskell qualification heuristics
haftmann [Mon, 22 Oct 2007 16:54:54 +0200] rev 25147
clarified Haskell qualification heuristics
2007-10-22 tuned abbreviations in class context
haftmann [Mon, 22 Oct 2007 16:54:52 +0200] rev 25146
tuned abbreviations in class context
2007-10-22 dropped superfluous inlining lemmas
haftmann [Mon, 22 Oct 2007 16:54:50 +0200] rev 25145
dropped superfluous inlining lemmas
2007-10-22 removed empty files;
wenzelm [Mon, 22 Oct 2007 15:27:11 +0200] rev 25144
removed empty files;
2007-10-22 abbrevs within inductive definitions may no longer depend on each other (reflects in internal organization, particularly for output);
wenzelm [Mon, 22 Oct 2007 15:24:58 +0200] rev 25143
abbrevs within inductive definitions may no longer depend on each other (reflects in internal organization, particularly for output);
2007-10-22 added @{sort}, @{type_syntax} antiquotations;
wenzelm [Mon, 22 Oct 2007 15:24:55 +0200] rev 25142
added @{sort}, @{type_syntax} antiquotations;
2007-10-22 >0 -> ~=0
nipkow [Mon, 22 Oct 2007 13:59:41 +0200] rev 25141
>0 -> ~=0
2007-10-21 More changes from >0 to ~=0::nat
nipkow [Sun, 21 Oct 2007 22:33:35 +0200] rev 25140
More changes from >0 to ~=0::nat
2007-10-21 tuned
urbanc [Sun, 21 Oct 2007 19:32:19 +0200] rev 25139
tuned
2007-10-21 further comments
urbanc [Sun, 21 Oct 2007 19:12:05 +0200] rev 25138
further comments
2007-10-21 polished the proofs and added a version of the weakening lemma that does not use the variable convention
urbanc [Sun, 21 Oct 2007 19:04:53 +0200] rev 25137
polished the proofs and added a version of the weakening lemma that does not use the variable convention
2007-10-21 fixed proof: neq0_conv;
wenzelm [Sun, 21 Oct 2007 17:48:11 +0200] rev 25136
fixed proof: neq0_conv;
2007-10-21 modernized specifications ('definition', 'axiomatization');
wenzelm [Sun, 21 Oct 2007 16:27:42 +0200] rev 25135
modernized specifications ('definition', 'axiomatization');
2007-10-21 Eliminated most of the neq0_conv occurrences. As a result, many
nipkow [Sun, 21 Oct 2007 14:53:44 +0200] rev 25134
Eliminated most of the neq0_conv occurrences. As a result, many theorems had to be rephrased with ~= 0 instead of > 0.
2007-10-21 context_const_ast_tr: proper const_syntax_name (cf. @{const_syntax});
wenzelm [Sun, 21 Oct 2007 14:21:54 +0200] rev 25133
context_const_ast_tr: proper const_syntax_name (cf. @{const_syntax});
2007-10-21 removed obsolete ML bindings;
wenzelm [Sun, 21 Oct 2007 14:21:53 +0200] rev 25132
removed obsolete ML bindings;
2007-10-21 modernized specifications ('definition', 'abbreviation', 'notation');
wenzelm [Sun, 21 Oct 2007 14:21:48 +0200] rev 25131
modernized specifications ('definition', 'abbreviation', 'notation');
2007-10-21 avoid very slow metis invocation;
wenzelm [Sun, 21 Oct 2007 14:21:45 +0200] rev 25130
avoid very slow metis invocation;
2007-10-21 misc tuning;
wenzelm [Sun, 21 Oct 2007 14:21:44 +0200] rev 25129
misc tuning;
2007-10-21 Fixed Bug in instantiation of Groebner Bases to field: dest_const used to raise TERM where the tactic handles ERROR
chaieb [Sun, 21 Oct 2007 12:33:12 +0200] rev 25128
Fixed Bug in instantiation of Groebner Bases to field: dest_const used to raise TERM where the tactic handles ERROR
2007-10-21 tuned the entry about nominal datatypes
urbanc [Sun, 21 Oct 2007 02:49:16 +0200] rev 25127
tuned the entry about nominal datatypes
2007-10-20 updated versions;
wenzelm [Sat, 20 Oct 2007 20:33:58 +0200] rev 25126
updated versions;
2007-10-20 discontinued support for 4.1.1, 4.1.2;
wenzelm [Sat, 20 Oct 2007 20:33:06 +0200] rev 25125
discontinued support for 4.1.1, 4.1.2; maintain PolyML.Compiler.printInAlphabeticalOrder;
2007-10-20 maintain PolyML.Compiler.printInAlphabeticalOrder in polyml.ML;
wenzelm [Sat, 20 Oct 2007 20:32:23 +0200] rev 25124
maintain PolyML.Compiler.printInAlphabeticalOrder in polyml.ML;
(0) -10000 -3000 -1000 -300 -100 -50 -24 +24 +50 +100 +300 +1000 +3000 +10000 +30000 tip