2007-10-22 wenzelm 2007-10-22 tuned;
2007-10-22 wenzelm 2007-10-22 fixed proof: no one_is_Suc_zero;
2007-10-22 wenzelm 2007-10-22 tuned Nominal entry;
2007-10-22 haftmann 2007-10-22 clarified Haskell qualification heuristics
2007-10-22 haftmann 2007-10-22 tuned abbreviations in class context
2007-10-22 haftmann 2007-10-22 dropped superfluous inlining lemmas
2007-10-22 wenzelm 2007-10-22 removed empty files;
2007-10-22 wenzelm 2007-10-22 abbrevs within inductive definitions may no longer depend on each other (reflects in internal organization, particularly for output);
2007-10-22 wenzelm 2007-10-22 added @{sort}, @{type_syntax} antiquotations;
2007-10-22 nipkow 2007-10-22 >0 -> ~=0
2007-10-21 nipkow 2007-10-21 More changes from >0 to ~=0::nat
2007-10-21 urbanc 2007-10-21 tuned
2007-10-21 urbanc 2007-10-21 further comments
2007-10-21 urbanc 2007-10-21 polished the proofs and added a version of the weakening lemma that does not use the variable convention
2007-10-21 wenzelm 2007-10-21 fixed proof: neq0_conv;
2007-10-21 wenzelm 2007-10-21 modernized specifications ('definition', 'axiomatization');
2007-10-21 nipkow 2007-10-21 Eliminated most of the neq0_conv occurrences. As a result, many theorems had to be rephrased with ~= 0 instead of > 0.
2007-10-21 wenzelm 2007-10-21 context_const_ast_tr: proper const_syntax_name (cf. @{const_syntax});
2007-10-21 wenzelm 2007-10-21 removed obsolete ML bindings;
2007-10-21 wenzelm 2007-10-21 modernized specifications ('definition', 'abbreviation', 'notation');
2007-10-21 wenzelm 2007-10-21 avoid very slow metis invocation;
2007-10-21 wenzelm 2007-10-21 misc tuning;
2007-10-21 chaieb 2007-10-21 Fixed Bug in instantiation of Groebner Bases to field: dest_const used to raise TERM where the tactic handles ERROR
2007-10-21 urbanc 2007-10-21 tuned the entry about nominal datatypes
2007-10-20 wenzelm 2007-10-20 updated versions;
2007-10-20 wenzelm 2007-10-20 discontinued support for 4.1.1, 4.1.2; maintain PolyML.Compiler.printInAlphabeticalOrder;
2007-10-20 wenzelm 2007-10-20 maintain PolyML.Compiler.printInAlphabeticalOrder in polyml.ML;
2007-10-20 wenzelm 2007-10-20 discontinued support for 4.1.1, 4.1.2;
2007-10-20 wenzelm 2007-10-20 moved internalM to PrintMode.internal; PrintMode.input;
2007-10-20 wenzelm 2007-10-20 tuned abbrev interface; PrintMode.internal;
2007-10-20 wenzelm 2007-10-20 tuned abbrev interface;
2007-10-20 wenzelm 2007-10-20 added fixed_abbrev;
2007-10-20 wenzelm 2007-10-20 added input/internal, which are never active in print_mode_value;
2007-10-20 wenzelm 2007-10-20 no_variables: tuned error msg;
2007-10-20 wenzelm 2007-10-20 PrintMode.internal;
2007-10-20 wenzelm 2007-10-20 tuned;
2007-10-20 wenzelm 2007-10-20 add_inductive: more careful handling of abbrevs -- do not expand prematurely;
2007-10-20 wenzelm 2007-10-20 fixed proof: neq0_conv;
2007-10-20 chaieb 2007-10-20 fixed proofs
2007-10-20 chaieb 2007-10-20 neq0_conv removed from [iff] -- causes problems by simple goals with blast, auto etc...
2007-10-19 wenzelm 2007-10-19 export_code: proper command;
2007-10-19 wenzelm 2007-10-19 warn_open: context position;
2007-10-19 wenzelm 2007-10-19 sorry: proper command;
2007-10-19 wenzelm 2007-10-19 tuned proofs: avoid implicit prems;
2007-10-19 wenzelm 2007-10-19 tuned proofs;
2007-10-19 wenzelm 2007-10-19 internal tuning: class_target, fork_mixfix, declare_const (singleton), abbrev;
2007-10-19 wenzelm 2007-10-19 tuned interfaces;
2007-10-19 haftmann 2007-10-19 tuned
2007-10-19 haftmann 2007-10-19 antisymmetry not a default intro rule any longer
2007-10-19 haftmann 2007-10-19 now employing dictionaries
2007-10-19 haftmann 2007-10-19 added examples
2007-10-19 haftmann 2007-10-19 lemmas with normalization
2007-10-19 wenzelm 2007-10-19 tuned CRITICAL markups;
2007-10-19 wenzelm 2007-10-19 do not export standard_infer_types;
2007-10-19 haftmann 2007-10-19 clarified abbreviations in class context
2007-10-19 ballarin 2007-10-19 Interpretation equations may have name and/or attribute; improved printing of types in interpretations.
2007-10-19 ballarin 2007-10-19 Interpretation equations may have name and/or attribute.
2007-10-19 krauss 2007-10-19 updated
2007-10-19 krauss 2007-10-19 removed funny formatting
2007-10-19 krauss 2007-10-19 Updated function tutorial: Types can be inferred and need not be given anymore