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!);