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;

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;

renamed Consts.the_declaration to Consts.the_type;

renamed the_declaration to the_type; added type_scheme, which covers proper consts and abbreviations (like typargs); tuned;

tuned

swapped constant components

canonical interpretation interface

prefer first constant component on merge

explicit parameter for class finite

tuned comment;

more on authentic syntax;

updated method "ferrack";

interpreter for List.append added again

quick_and_dirty (again) not touched anymore

require_thy: read_text *after* checking parents (otherwise outdating an existing descendant will leave the dependencies corrupted);

gen_add_inductive_i: treat abbrevs as local defs, expand by export; tuned;

tuned various Class interfaces; tuned;

removed obsolete Class.class_of_locale/locale_of_class;

tuned;

added add_def;

added is_class; tuned signature of add_const/abbrev_in_class; removed obsolete class_of_locale/locale_of_class; tuned name prefixing: Sign.full_name does the job;

PolyML.Compiler.maxInlineSize := 80;

abbrev: return hypothetical def; replaced obsolete Theory.add_finals_i by Theory.add_deps; misc cleanup;

renamed def to define; abbrev: return hypothetical def;

(un)overload: full rewrite; use Attrib.attribute_i for internal args; misc tuning;

add_abbrevs: unvarify result;

replaced obsolete Theory.add_finals_i by Theory.add_deps;

Theory.specify_const: added deps argument;

renamed LocalTheory.def to LocalTheory.define;

typo in comment fixed

significant code overhaul, bugfix for inductive data types

added generic provide_file; tuned;

pass explicit target record -- more informative peek operation; removed obsolete hide_abbrev; misc tuning;

more informative TheoryTarget.peek operation;

fork_mixfix: explicit bool argument;

eval_term: moved actual evaluation out of CRITICAL section;

preventing eta-redexes in theorems from causing failure

trying to make it run faster

calling the correct interface

replaced syntax/translations by abbreviation;

updated

dropped local_syntax

tuned

(intermediate quickfix)

removed

added

metis calls

updated

moved class power to theory Power

refined; moved class power to theory Power

consolidated naming conventions for code generator theories

class div inherits from class times

code_include replaces code_moduleprolog

added subclass command

enabled Refute_Examples again;

local_axioms: impose hyps stemming from local consts as well (otherwise the axioms will be more general than expected!);

disabled Refute_Examples temporarily;

local_theory: incorporated consts into axioms; LocalDefs.expand_cterm; tuned;

removed unused/impure quiet_mode; local_theory: incorporated consts into axioms; tuned;

added export_cterm; tuned;

local_theory: incorporated consts into axioms;

replaced Term.equiv_types by Type.similar_types; moved add_axiom/def to more_thm.ML;

replaced Term.equiv_types by Type.similar_types;

dest/cert_def: replaced Pretty.pp by explicit Proof.context;

added elim_implies (more convenient argument order); added unvarify (from drule.ML); added specification primitives: add_axiom, add_def;

removed obsolete flip;

moved Drule.unvarify to Thm.unvarify (cf. more_thm.ML); tuned;

replaced (flip Thm.implies_elim) by Thm.elim_implies;

moved Drule.unvarify to Thm.unvarify (cf. more_thm.ML);

usedir: added HOL_USEDIR_OPTIONS;

reconstruction bug fix

tuned;

replaced Sign.add_consts_i by Sign.declare_const;

replaced Sign.add_consts_authentic by Sign.declare_const; tuned;

renamed Syntax.XXX_mode to Syntax.mode_XXX; moved ProofContext.pp to Syntax.pp;

removed obsolete AxClass.params_of_class; tuned;

replaced Sign.add_consts_authentic by Sign.declare_const; replaced read_param by Sign.read_const, which is independent of syntax; added define_class_params (from axclass.ML);

load axclass.ML before Isar; load subclass.ML earlier;

added specify_const;

removed obsolete simple_def;

moved define_class_params to Isar/class.ML; removed obsolete params_of_class, print_axclasses; moved ProofContext.pp to Syntax.pp; misc tuning;

load axclass.ML before Isar;

Theory.specify_const;

moved ProofContext.pp to Syntax.pp;

renamed Syntax.XXX_mode to Syntax.mode_XXX;

replaced Sign.add_consts_authentic by Sign.declare_const;

rationalized redundant code

usage: HOL_USEDIR_OPTIONS;

failure messages

'notation': allow structmixfix;

update_modesyntax: may delete 'structure' notation as well;

'notation': allow 'structure' as well;

removed redundant strip_vars/abs_eqn, use improved Drule.abs_def instead; renamed cert_instantiations to check_instantiations, check input only once (simultaneously!);

replaced add_modesyntax by general update_modesyntax (add or del); tuned;

added 'no_notation';

generalized notation interface (add or del);

tuned;

improved abs_def: only abstract over outermost (unique) Vars;

proper latex antiquotations instead of adhoc escapes;

updated;

added no_notation;

removed dead code

more metis proofs

Prepare proper interface of interpretation_i, interpret_i.

getting rid of type typ_var

tuned;

class: print result is for locale;

context-based treatment of generalization; also handling TFrees in axiom clauses

TheoryTarget.init_cmd;

removed LocalTheory.defs/target_morphism operations; moved target_morphism to local_theory.ML; renamed init_i to init, and init to init_cmd; tuned;

renamed AxClass.get_definition to AxClass.get_info (again); simplified goal setup using Proof.theorem_i;

removed LocalTheory.defs/target_morphism operations; added target_morphism (from theory_target.ML);

AxClass.axiomatize and Specification: renamed XXX_i to XXX, and XXX to XXX_cmd;

removed LocalTheory.defs/target_morphism operations;

renamed AxClass.get_definition to AxClass.get_info (again); tuned intro_classes_tac;

renamed AxClass.get_definition to AxClass.get_info (again); AxClass.axiomatize: renamed XXX_i to XXX, and XXX to XXX_cmd;

renamed AxClass.get_definition to AxClass.get_info (again);

Specification: renamed XXX_i to XXX, and XXX to XXX_cmd;

AxClass.axiomatize: renamed XXX_i to XXX, and XXX to XXX_cmd;

removed LocalTheory.defs, use plain LocalTheory.def;

tuned;

generic Syntax.pretty/string_of operations; added uncheck/unparse_classrel/arity (from sign.ML); tuned;

generic Syntax.pretty/string_of operations; proper installation of unparsers and term_uncheck (contract_abbrevs); removed obsolete pretty/string_of_term/typ/sort/classrel/arity (cf. structure Syntax); tuned;

generic Syntax.pretty/string_of operations; existing pretty_term = Syntax.pretty_term o ProofContext.init etc.; removed pretty_classrel/arity (cf. Syntax/syntax.ML);

generic Syntax.pretty/string_of operations;

updated keywords

moved translation kernel to CodeThingol

tuned

simplified evaluation

integrated FixedPoint into Inductive

added proper subclass concept; improved class target

fixed bug in grobner_ideal

tuned generated comment;

primitive add_def: strip sorts in axiom;

avoid polymorphic equality;