Added reference to Jeremy Dawson's paper on the word library. Added header to remaining word/*.thy files so they show up in toc.

recdef -> fun

added Fun

tuned

recdef -> fun

*** empty log message ***

Catch exceptions arising during the abstraction operation. Filter out theorems that are "too deep".

Added example for the ideal membership problem solved by algebra

Added field ideal into entry - uses by algebra method to prove the ideal membership problem

changed signature according to normalizer_data.ML

tuned

(1) signatures updated according to normalizer_data.ML (added field ideal in entry); (2) For a theory the conversions returned are now ring_conv (as before, proves a universal statement), simple_ideal proves ideal membership for one polynomial ; multi_ideal solves the more general ideal membership for several existentially quantifier variables involved in several conjunctions; a simpset containing a simproc to turn x = y into p = 0 where p is the normal form of x - y; (3) Added ideal_tac a tactic to prove general ideal membership (cf. John Harrision CADE 2007) ; (4) Added algebra_tac : first tries ring_tac (old algebra) then ideal_tac

(1) added axiom to ringb and theorems to enable algebra to prove the ideal membership problem; (2) Method algebra now calls algebra_tac which first tries to solve a universal formula, then in case of failure trie to solve the ideal membership problem (see HOL/Tools/Groebner_Basis/groebner.ML)

exported field_comp_conv: a numerical conversion over fields

dropped AxClass

tuned

Handle Subscript exception when looking up bound variables.

Added well-formedness check to Abst case in function prf_of.

added omission

bugfixes concerning strange theorems

fixed typo

const antiquotation clarified

clarified

handling of notation in class target

fixed document preparation

improved website integration

adjusted

split library index into templates

split library index into templates

structured

tidied version

simplified proof

continued localization

fixed typo

added nbe

test_proof: do not change Proofterm.proofs here (not thread-safe);

improved notion of 'nicer' fact names (observe some name space properties);

export is_hidden;

added bool_ord;

qualified Proofterm.proofs;

fun/function: generate case names for induction rules

append/member: more light-weight way to declare authentic syntax; tuned proofs;

made SML/NJ happy;

safe_exit: controlled_execution;

better compute oracle

better compute oracle

adapted Compute...

use "fun" for definition of "member" -> authentic syntax

ASCIIfied README

added list comprehension syntax

locale_const: in_class workaround prevents additional locale version of class consts;

notation: associate syntax to checked-unchecked term;

export class_prefix; removed obsolete const hiding;

tuned

changed order of class parameters

dropped square syntax

localized monotonicity; tuned syntax

dropped "brown" syntax

replaced Secure.evaluate by ML_Context.evaluate;

asm_rewrite_goal_tac: avoiding PRIMITIVE lets informative exceptions (from simprocs) get through;

proven witness: proper Goal.close_result save huge amounts of resources when using proof terms;

print the defined constants when finished; tuned

adjusted

tuned

added NEWS entry for function package

added hint for algebra

moved primitive operations to class.ML

fixed syntax; truned code structure; added primitive subclass interface with consideraton of syntax etc.

dropped redundancy

various localizations

made command 'undo' silent ('ProofGeneral.undo' becomes a historical relic);

tuned

clarified implementation

propagation through class hierarchy

added function for evaluation by compiler invocation

more computation with rationals

localized further

continued

tuned

THIS_IS_ISABELLE_MAKEBIN;

updated;

README for polyml-5.1 binary distribution;

avoid very slow metis invocation (saves 1min on 1.60 GHz machine);

separate RecordPackage.timing flag;

tuned;

tuned file names etc.;

*** empty log message ***

added HOL-Statespace session;

be explicit about .ML files;

fixed HOL-Statespace for case-sensitive file-system;

tuned comments;

added Statespace library

tuned

fun command: use "reinit" between "function" and "termination"

parse_term: invoke full Syntax.check_term, not just standard_infer_types;

fixed typo

added subclass_rule

example with rational numbers

dropped superfluous inlining rule

tuned

went back to >0

changed back from ~=0 to >0

updated;

added XCONST syntax (keeps original spelling of const);

translations: use XCONST for input patterns (keeps original spelling of const);

random tidying of proofs

empty files are back -- referenced in Makefile;

dropped code redundancy

tuned

tuned proof

partially localized

continued

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;

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;