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;

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;