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;

tuned abbrev interface;

added fixed_abbrev;

added input/internal, which are never active in print_mode_value;

no_variables: tuned error msg;

PrintMode.internal;

tuned;

add_inductive: more careful handling of abbrevs -- do not expand prematurely;

fixed proof: neq0_conv;