2001-02-12 wenzelm 2001-02-12 tuned;
2001-02-12 wenzelm 2001-02-12 support \<subseteq> syntax in classes/classrel/axclass/instance;
2001-02-12 wenzelm 2001-02-12 \<subseteq> syntax for classes/classrel/axclass/instance;
2001-02-12 wenzelm 2001-02-12 \<subseteq>;
2001-02-11 wenzelm 2001-02-11 added "xsymbols" syntax for "=?=";
2001-02-11 wenzelm 2001-02-11 more robust selection of calculational rules;
2001-02-11 wenzelm 2001-02-11 tuned trans rules;
2001-02-11 wenzelm 2001-02-11 updated;
2001-02-11 wenzelm 2001-02-11 tuned;
2001-02-10 ballarin 2001-02-10 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.
2001-02-10 ballarin 2001-02-10 Definition of setsum (sort constraint) relaxed to {zero, plus}.
2001-02-10 ballarin 2001-02-10 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}.
2001-02-09 wenzelm 2001-02-09 tuned;
2001-02-09 wenzelm 2001-02-09 lower priority for forw_subst;
2001-02-09 wenzelm 2001-02-09 tuned;
2001-02-09 kleing 2001-02-09 not used any more (all Isar style)
2001-02-09 kleing 2001-02-09 removed MicroJava/Digest.thy
2001-02-09 kleing 2001-02-09 tuned for 99-2 release
2001-02-09 wenzelm 2001-02-09 unsymbolized; tuned;
2001-02-07 wenzelm 2001-02-07 tuned;
2001-02-07 wenzelm 2001-02-07 improved;
2001-02-07 oheimb 2001-02-07 solved non-initialization problems; improvements using prefer
2001-02-07 paulson 2001-02-07 various revisions in response to comments from Tobias
2001-02-07 wenzelm 2001-02-07 val get_goal: state -> context * (thm list * thm);
2001-02-06 wenzelm 2001-02-06 4.0 version;
2001-02-06 paulson 2001-02-06 snapshot of a new version
2001-02-06 paulson 2001-02-06 new theorem Transset_iff_Union_subset
2001-02-06 kleing 2001-02-06 tuned
2001-02-05 wenzelm 2001-02-05 improved;
2001-02-05 wenzelm 2001-02-05 polyml multiplatform setup;
2001-02-05 wenzelm 2001-02-05 tuned
2001-02-05 wenzelm 2001-02-05 tuned;
2001-02-05 oheimb 2001-02-05 improved document (added headers etc)
2001-02-05 wenzelm 2001-02-05 tuned
2001-02-05 oheimb 2001-02-05 improvements concerning instantiations etc.
2001-02-05 wenzelm 2001-02-05 disable non-existant chapters
2001-02-05 wenzelm 2001-02-05 tuned;
2001-02-05 wenzelm 2001-02-05 fixed version string;
2001-02-05 wenzelm 2001-02-05 polyml-3.x.ML vs polyml-4.0.ML;
2001-02-05 wenzelm 2001-02-05 renamed polyml.ML to polyml-3.x.ML and polyml-4.0.ML to polyml.ML (default);
2001-02-05 wenzelm 2001-02-05 tuned;
2001-02-05 wenzelm 2001-02-05 example Proof General settings;
2001-02-04 wenzelm 2001-02-04 document setup;
2001-02-04 wenzelm 2001-02-04 converted to new-style;
2001-02-04 wenzelm 2001-02-04 moved theory Perm to HOL/Library;
2001-02-04 wenzelm 2001-02-04 added no_document
2001-02-04 wenzelm 2001-02-04 tuned
2001-02-04 wenzelm 2001-02-04 added Permutation;
2001-02-04 wenzelm 2001-02-04 moved from Induct/ to Library/
2001-02-04 wenzelm 2001-02-04 updated
2001-02-04 wenzelm 2001-02-04 added no_document;
2001-02-04 wenzelm 2001-02-04 updated split_format;
2001-02-04 wenzelm 2001-02-04 * no_document ML operator temporarily disables LaTeX document generation;
2001-02-04 wenzelm 2001-02-04 HOL-NumberTheory: converted to new-style format and proper document setup;
2001-02-03 wenzelm 2001-02-03 tuned msg;
2001-02-03 wenzelm 2001-02-03 tuned;
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)';