2001-02-03 wenzelm 2001-02-03 Induct: converted some theories to new-style format;
2001-02-03 wenzelm 2001-02-03 fixed syntax of 'split_format';
2001-02-03 wenzelm 2001-02-03 use fgrep;
2001-02-03 wenzelm 2001-02-03 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)';
2001-02-03 paulson 2001-02-03 commutation theory, ported by Sidi Ehmety
2001-02-03 wenzelm 2001-02-03 updated;
2001-02-03 wenzelm 2001-02-03 simplified 'split_format' syntax;
2001-02-02 wenzelm 2001-02-02 'split_format' attribute;
2001-02-02 wenzelm 2001-02-02 tuned;
2001-02-02 wenzelm 2001-02-02 module setup; use hidden internal_split constants;
2001-02-02 wenzelm 2001-02-02 use hol_simplify;
2001-02-02 wenzelm 2001-02-02 use hol_rewrite_cterm;
2001-02-02 wenzelm 2001-02-02 added hol_simplify, hol_rewrite_cterm;
2001-02-02 wenzelm 2001-02-02 split = split_conv (for compatibility);
2001-02-02 wenzelm 2001-02-02 added hidden internal_split constant; tuned;
2001-02-02 wenzelm 2001-02-02 isatool convert;
2001-02-02 paulson 2001-02-02 new theorem fib_mult_eq_setsum
2001-02-02 oheimb 2001-02-02 little bugfixes; added induct_thm_tac
2001-02-01 wenzelm 2001-02-01 moved to Product_Type_lemmas.ML
2001-02-01 oheimb 2001-02-01 added translations for bind_thm and val
2001-02-01 oheimb 2001-02-01 converted to Isar, simplifying recursion on class hierarchy
2001-02-01 oheimb 2001-02-01 converted to Isar therory, adding attributes complete_split and split_format
2001-02-01 wenzelm 2001-02-01 converted to new-style theories;
2001-02-01 wenzelm 2001-02-01 updated
2001-02-01 wenzelm 2001-02-01 ext_classrel: certify_class;
2001-02-01 wenzelm 2001-02-01 comment
2001-02-01 wenzelm 2001-02-01 tuned
2001-02-01 wenzelm 2001-02-01 tuned;
2001-02-01 wenzelm 2001-02-01 added "numerals" theorems;
2001-02-01 wenzelm 2001-02-01 thms_containing: term args;
2001-02-01 wenzelm 2001-02-01 * Pure: 'thms_containing' now takes actual terms as arguments; * isatool convert assists in eliminating legacy ML scripts;
2001-02-01 oheimb 2001-02-01 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
2001-02-01 oheimb 2001-02-01 debugged declare
2001-02-01 oheimb 2001-02-01 further minor improvements
2001-01-31 wenzelm 2001-01-31 strip_blanks moved to General/symbol.ML;
2001-01-31 wenzelm 2001-01-31 pretty_text: tweak_lines handles linebreaks gracefully;
2001-01-31 wenzelm 2001-01-31 added strip_blanks;
2001-01-31 oheimb 2001-01-31 added attribute declarations, etc.
2001-01-31 oheimb 2001-01-31 improved theory reference in comment
2001-01-31 oheimb 2001-01-31 added diff_single_insert and subset_image_iff
2001-01-31 oheimb 2001-01-31 shortened proof of some1_equality
2001-01-31 wenzelm 2001-01-31 more robust handling of rule cases hints;
2001-01-30 wenzelm 2001-01-30 tuned;
2001-01-30 oheimb 2001-01-30 added if_def2
2001-01-30 oheimb 2001-01-30 added foldln
2001-01-30 oheimb 2001-01-30 corrected file name suffixes
2001-01-30 oheimb 2001-01-30 removed (obsolete) mult_assumption
2001-01-30 berghofe 2001-01-30 Fixed bug in complete_split_rule_var.
2001-01-30 wenzelm 2001-01-30 tuned;
2001-01-29 wenzelm 2001-01-29 avoid dead code;
2001-01-29 nipkow 2001-01-29 Moved some thms from Transitive_ClosureTr.ML to Transitive_Closure.thy
2001-01-29 nipkow 2001-01-29 *** empty log message ***
2001-01-29 nipkow 2001-01-29 *** empty log message ***
2001-01-29 wenzelm 2001-01-29 added Unix example;
2001-01-29 wenzelm 2001-01-29 updated;
2001-01-29 wenzelm 2001-01-29 *** empty log message ***
2001-01-29 berghofe 2001-01-29 Completely split rule eval_evals_exec.induct before applying it.
2001-01-29 berghofe 2001-01-29 New function complete_split_rule for complete splitting of partially splitted rules (as generated by inductive definition package).
2001-01-29 berghofe 2001-01-29 Splitting of arguments of product types in induction rules is now less aggressive.
2001-01-29 paulson 2001-01-29 fixed the pr example