Changes to HOL/Algebra: - Axclasses consolidated (axiom one_not_zero). - Now uses summation operator setsum; SUM has been removed. - Priority of infix assoc changed to 50, in accordance to dvd.

Definition of setsum (sort constraint) relaxed to {zero, plus}.

Updates to HOL/Algebra: - axclasses consolidated (lemma one_not_zero) - summation operator SUM removed, now uses setsum Use of setsum made it necessary to relax sort constraint in its definition to {zero, plus}.

tuned;

lower priority for forw_subst;

tuned;

not used any more (all Isar style)

removed MicroJava/Digest.thy

tuned for 99-2 release

unsymbolized; tuned;

tuned;

improved;

solved non-initialization problems; improvements using prefer

various revisions in response to comments from Tobias

val get_goal: state -> context * (thm list * thm);

4.0 version;

snapshot of a new version

new theorem Transset_iff_Union_subset

tuned

improved;

polyml multiplatform setup;

tuned

tuned;

improved document (added headers etc)

tuned

improvements concerning instantiations etc.

disable non-existant chapters

tuned;

fixed version string;

polyml-3.x.ML vs polyml-4.0.ML;

renamed polyml.ML to polyml-3.x.ML and polyml-4.0.ML to polyml.ML (default);

tuned;

example Proof General settings;

document setup;

converted to new-style;

moved theory Perm to HOL/Library;

added no_document

tuned

added Permutation;

moved from Induct/ to Library/

updated

added no_document;

updated split_format;

* no_document ML operator temporarily disables LaTeX document generation;

HOL-NumberTheory: converted to new-style format and proper document setup;

tuned msg;

tuned;

Induct: converted some theories to new-style format;

fixed syntax of 'split_format';

use fgrep;

HOL: inductive package no longer splits induction rule aggressively, but only as far as specified by the introductions given; the old format may recovered via ML function complete_split_rule or attribute 'split_rule (complete)';

commutation theory, ported by Sidi Ehmety

updated;

simplified 'split_format' syntax;

'split_format' attribute;

tuned;

module setup; use hidden internal_split constants;

use hol_simplify;

use hol_rewrite_cterm;

added hol_simplify, hol_rewrite_cterm;

split = split_conv (for compatibility);

added hidden internal_split constant; tuned;

isatool convert;

new theorem fib_mult_eq_setsum

little bugfixes; added induct_thm_tac

moved to Product_Type_lemmas.ML

added translations for bind_thm and val

converted to Isar, simplifying recursion on class hierarchy

converted to Isar therory, adding attributes complete_split and split_format

converted to new-style theories;

updated

ext_classrel: certify_class;

comment

tuned

tuned;

added "numerals" theorems;

thms_containing: term args;

* Pure: 'thms_containing' now takes actual terms as arguments; * isatool convert assists in eliminating legacy ML scripts;

added sum_case_map_upd_empty, sum_case_empty_map_upd, and sum_case_map_upd_map_upd (also to default simpset), added map_of_map

debugged declare

further minor improvements

strip_blanks moved to General/symbol.ML;

pretty_text: tweak_lines handles linebreaks gracefully;

added strip_blanks;

added attribute declarations, etc.

improved theory reference in comment

added diff_single_insert and subset_image_iff

shortened proof of some1_equality

more robust handling of rule cases hints;

tuned;

added if_def2

added foldln

corrected file name suffixes

removed (obsolete) mult_assumption

Fixed bug in complete_split_rule_var.

tuned;

avoid dead code;

Moved some thms from Transitive_ClosureTr.ML to Transitive_Closure.thy

*** empty log message ***

*** empty log message ***

added Unix example;

updated;

*** empty log message ***

Completely split rule eval_evals_exec.induct before applying it.

New function complete_split_rule for complete splitting of partially splitted rules (as generated by inductive definition package).

Splitting of arguments of product types in induction rules is now less aggressive.

fixed the pr example

simplified gcd

fixed set comprehension print translation

Merged Example into While_Combi

*** empty log message ***

renamed to Transitive_Closure_lemmas.ML;

tuned;

Transitive_Closure turned into new-style theory;

tuned;

*** empty log message ***

added Martin Strecker, Christian Buttenberg, Alexandra Kirsch and project Verificard

* Document preparation: renamed standard symbols \<ll> to \<lless> and \<gg> to \<ggreater>;

added eufrak symbols; renamed \<ll> to \<lless> and \<gg> to \<ggreater>;

more symbols;