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;

fixed proofs

neq0_conv removed from [iff] -- causes problems by simple goals with blast, auto etc...

export_code: proper command;

warn_open: context position;

sorry: proper command;

tuned proofs: avoid implicit prems;

tuned proofs;

internal tuning: class_target, fork_mixfix, declare_const (singleton), abbrev;

tuned interfaces;

tuned

antisymmetry not a default intro rule any longer

now employing dictionaries

added examples

lemmas with normalization

tuned CRITICAL markups;

do not export standard_infer_types;

clarified abbreviations in class context

Interpretation equations may have name and/or attribute; improved printing of types in interpretations.

Interpretation equations may have name and/or attribute.

updated

removed funny formatting

Updated function tutorial: Types can be inferred and need not be given anymore

98% localized

dropped doubled proof

Simultaneous type inference using read_specification

some more metis calls

Improving the propagation of type constraints for Frees

Ensured that the right number of ATP calls is generated

CRITICAL evaluation

improved class syntax

tuned

DeclareRobustCommand \isactrlbsub/esub etc.;

evaluation is CRITICAL

moved fork_mixfix to theory_target

moved lemmas to OrderedGroup.thy

continued localization

localized mono predicate

removed obsolete unlocalize_mfix;

removed obsolete unlocalize_mixfix;

locale pred: authentic syntax, tuned aprop_tr' accordingly;

store external accesses within name space (as produced by naming policy); improved sticky_prefix: suppress redundant accesses to achieve shorter output; removed unused interfaces; replaced accesses' by external_names (depening on naming);

removed unused set_policy;

replaced NameSpace.accesses' by NameSpace.external_names (depening on naming);

added sorted_list_of_set

tuned fork_mixfix (back from class.ML);

clarified naming conventions of 'parse' and 'check' (as opposed to former 'cert');

removed obsolete fork_mixfix (back to theory_target.ML);

updated;

clarified fork_mixfix

exported standard_term_check

global class syntax

added yield_singleton

Syntax.(un)check: explicit result option;

apply_wrappers: perhaps_apply/loop;

added perhaps_apply/loop;

Mark A. Hillebrand, DFKI: Robust sub/superscripts in LaTeX document output.

updated;

DeclareRobustCommand isascriptstyle (enables sub/superscripts within section headings etc.);

tuned Const.the_abbreviation;

misc cleanup of abbrev/local_const;

added revert_abbrev; contract_abbrevs: ignore Syntax.internalM (changed meaning of this special case); print_abbrevs: proper treatment of global consts (after local/global swap);

add_bind: close_schematic_term;

tuned hidden_polymorphism; added close_schematic_term;

add_abbrev: removed Logic.legacy_varifyT, do not unvarify result (again); added revert_abbrev;

the_abbreviation: return plain rhs only; force_expand: expand to plain rhs; added revert_abbrev; tuned;

added the "max_sledgehammers" option

Fixed variable naming in mutual induction rules

"sequential" is no longer a keyword. It is still used as before, but as a normal identifier => no pollution of keyword space

polished some comments

unparse_arity: unparse type constructor as well;