tuned;

fixed proof: no one_is_Suc_zero;

tuned Nominal entry;

clarified Haskell qualification heuristics

tuned abbreviations in class context

dropped superfluous inlining lemmas

removed empty files;

abbrevs within inductive definitions may no longer depend on each other (reflects in internal organization, particularly for output);

added @{sort}, @{type_syntax} antiquotations;

>0 -> ~=0

More changes from >0 to ~=0::nat

tuned

further comments

polished the proofs and added a version of the weakening lemma that does not use the variable convention

fixed proof: neq0_conv;

modernized specifications ('definition', 'axiomatization');

Eliminated most of the neq0_conv occurrences. As a result, many theorems had to be rephrased with ~= 0 instead of > 0.

context_const_ast_tr: proper const_syntax_name (cf. @{const_syntax});

removed obsolete ML bindings;

modernized specifications ('definition', 'abbreviation', 'notation');

avoid very slow metis invocation;

misc tuning;

Fixed Bug in instantiation of Groebner Bases to field: dest_const used to raise TERM where the tactic handles ERROR

tuned the entry about nominal datatypes

updated versions;

discontinued support for 4.1.1, 4.1.2; maintain PolyML.Compiler.printInAlphabeticalOrder;

maintain PolyML.Compiler.printInAlphabeticalOrder in polyml.ML;

discontinued support for 4.1.1, 4.1.2;

moved internalM to PrintMode.internal; PrintMode.input;

tuned abbrev interface; PrintMode.internal;