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;