2006-04-11 wenzelm 2006-04-11 added super_classes (from sorts.ML); removed read/cert_classrel (see axclass.ML);
2006-04-11 wenzelm 2006-04-11 added mk_classrel, dest_classrel, mk_arities, dest_arity (from axclass.ML); tuned;
2006-04-11 wenzelm 2006-04-11 moved abstract syntax operations to logic.ML; maintain class parameters; added params_of_sort; added cert/read_classrel (from sign.ML), check class parameters; tuned;
2006-04-10 obua 2006-04-10 Moved stuff from Ring_and_Field to Matrix
2006-04-10 berghofe 2006-04-10 Adapted to changed type of add_typedef_i.
2006-04-10 nipkow 2006-04-10 Hoare(Parallel) dependencies on document/*
2006-04-10 nipkow 2006-04-10 added references
2006-04-10 nipkow 2006-04-10 Minimal doc
2006-04-10 nipkow 2006-04-10 Included cyclic list examples
2006-04-10 haftmann 2006-04-10 fixed value restriction
2006-04-10 nipkow 2006-04-10 Added splicing algorithm.
2006-04-10 wenzelm 2006-04-10 hide (open) const;
2006-04-10 wenzelm 2006-04-10 simplified AxClass.add_axclass interface;
2006-04-10 wenzelm 2006-04-10 added aT (from axclass.ML); non-pervasive itselfT, a_itselfT;
2006-04-10 wenzelm 2006-04-10 removed unused class_le_path, sort_less;
2006-04-10 wenzelm 2006-04-10 add_axclass(_i): return class name only; subclass/arity statements: require actual TVars, store raw data; tuned;
2006-04-10 wenzelm 2006-04-10 Term.itselfT;
2006-04-09 nipkow 2006-04-09 Added function "splice"
2006-04-09 wenzelm 2006-04-09 Even/Odd: avoid clash with even/odd of Main HOL;
2006-04-09 wenzelm 2006-04-09 results: smart_pretty_thm uses adhoc proof context if possible;
2006-04-09 wenzelm 2006-04-09 added full_name; abbrevs: mode does not affect name space;
2006-04-09 wenzelm 2006-04-09 add_syntax: actually observe print mode;
2006-04-09 wenzelm 2006-04-09 print_term etc.: actually observe print mode in final output;
2006-04-09 wenzelm 2006-04-09 abbrevs: mode does not affect name space;
2006-04-09 wenzelm 2006-04-09 added coalesce;
2006-04-09 wenzelm 2006-04-09 moved theory presentation to Isar/ROOT.ML;
2006-04-09 wenzelm 2006-04-09 hide consts in Numeral.thy;
2006-04-09 wenzelm 2006-04-09 tuned syntax/abbreviations;
2006-04-09 wenzelm 2006-04-09 unfold(ed): not necessrily meta equations;
2006-04-09 nipkow 2006-04-09 Made "empty" an abbreviation.
2006-04-09 nipkow 2006-04-09 *** empty log message ***
2006-04-09 nipkow 2006-04-09 Removed old set interval syntax.
2006-04-08 wenzelm 2006-04-08 pretty_term: late externing of consts (support authentic syntax);
2006-04-08 wenzelm 2006-04-08 pretty: late externing of consts (support authentic syntax);
2006-04-08 wenzelm 2006-04-08 removed fix_mixfix; added const_mixfix, mixfix_const;
2006-04-08 wenzelm 2006-04-08 abbreviation(_i): do not expand abbreviations, do not use derived_def;
2006-04-08 wenzelm 2006-04-08 add_abbrevs(_i): support print mode; pretty_term': expand abbreviations only for well-typed terms; added expand_abbrevs; tuned;
2006-04-08 wenzelm 2006-04-08 abbrevs: support print mode;
2006-04-08 wenzelm 2006-04-08 simplified handling of authentic syntax (cf. early externing in consts.ML); simplified extern_term;
2006-04-08 wenzelm 2006-04-08 'abbreviation': optional print mode;
2006-04-08 wenzelm 2006-04-08 tuned;
2006-04-08 wenzelm 2006-04-08 pretty_term': early vs. late externing (support authentic syntax); add_abbrevs(_i): support print mode and authentic syntax;
2006-04-08 wenzelm 2006-04-08 print_theory: print abbreviations nicely;
2006-04-08 wenzelm 2006-04-08 added intern/extern/extern_early; added expand_abbrevs flag; strip_abss: demand ocurrences of bounds in body; const decl: added flag for early externing (disabled for authentic syntax); abbrevs: support print mode; major cleanup;
2006-04-08 wenzelm 2006-04-08 refined 'abbreviation';
2006-04-08 haftmann 2006-04-08 made symlink relative
2006-04-08 haftmann 2006-04-08 made symlink relative
2006-04-08 kleing 2006-04-08 converted Müller to Mueller to make smlnj 110.58 work
2006-04-07 berghofe 2006-04-07 Fixed bug that caused proof of induction rule to fail for inductive sets with trivial introduction rules such as "x : S ==> x : S".
2006-04-07 kleing 2006-04-07 remame ASeries to Arithmetic_Series
2006-04-07 berghofe 2006-04-07 Added alternative version of thms_of_proof that does not recursively descend into proofs of (named) theorems.
2006-04-07 mengj 2006-04-07 hash table now stores thm and get_clasimp_atp_lemmas returns thm rather than term.
2006-04-07 mengj 2006-04-07 filter now accepts axioms as thm, instead of term.
2006-04-07 mengj 2006-04-07 tptp_write_file accepts axioms as thm.
2006-04-07 mengj 2006-04-07 added another function for CNF.
2006-04-07 mengj 2006-04-07 lemmas returned from ResClasimp.get_clasimp_atp_lemmas are thm rather than term.
2006-04-07 kleing 2006-04-07 renamed ASeries to Arithmetic_Series, removed the ^M
2006-04-06 urbanc 2006-04-06 modified the perm_compose rule such that it is applied as simplification rule (as simproc) in the restricted case where the first permutation is a swapping coming from a supports problem also deleted the perm_compose' rule from the set of rules that are automatically tried
2006-04-06 haftmann 2006-04-06 cleanup in typedef/datatype package
2006-04-06 haftmann 2006-04-06 added explicit serialization for int equality