added wellorder axclass

moved inv_image to Relation

moved wf_less from Nat.ML to NatDef.ML

added nat as instance of new wellorder axclass

Ord.thy/.ML converted to Isar

added trial proof

improved subst_RS

added missiong word

*** empty log message ***

index mod syntax;

tuned;

isatool install -k;

handle KDE version 1 or 2;

isatool install handles KDE version 1 or 2;

removed whitespace

supressed some warnings on identical proofstate

adhoc script for creating complete Isabelle dist pages;

imp_cong2 -> imp_cong

new function get_overloads

updated the unicity proof

tidying

not_bad_tac is obsolete

a new theorem from Bryan Ford

added support for AddXIs, AddXEs, AddXDs

tuned;

tuned;

tuned;

\remarksfalse;

tuned;

swapped Fleuriot and Paulson

create dist packages;

partial conversion to Isar script style in HOL/Auth removes some .ML files

partial conversion to Isar script style in HOL/Auth removes some .ML files

partial conversion to Isar script style simplified unicity proofs

tuned;

tuned;

support \<subseteq> syntax in classes/classrel/axclass/instance;

\<subseteq> syntax for classes/classrel/axclass/instance;

\<subseteq>;

added "xsymbols" syntax for "=?=";

more robust selection of calculational rules;

tuned trans rules;

updated;

tuned;

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;