2001-11-24 wenzelm 2001-11-24 gen_merge_lists';
2001-11-24 wenzelm 2001-11-24 generic_merge;
2001-11-24 wenzelm 2001-11-24 converted simp lemmas;
2001-11-24 wenzelm 2001-11-24 tuned;
2001-11-24 berghofe 2001-11-24 Extended match_proof to handle abstractions.
2001-11-23 wenzelm 2001-11-23 tuned;
2001-11-23 wenzelm 2001-11-23 improved ordering of evaluated elements;
2001-11-23 wenzelm 2001-11-23 time_use_thy "Locales";
2001-11-23 nipkow 2001-11-23 Isar conversion
2001-11-22 wenzelm 2001-11-22 theory Locales temporarily disabled;
2001-11-22 wenzelm 2001-11-22 beginnings of actual locale expressions;
2001-11-22 wenzelm 2001-11-22 improved locale expression syntax;
2001-11-22 wenzelm 2001-11-22 locale expression import;
2001-11-22 wenzelm 2001-11-22 import locale expression;
2001-11-22 wenzelm 2001-11-22 tuned;
2001-11-22 wenzelm 2001-11-22 added uname; syntax for locale expressions (presently unused);
2001-11-22 wenzelm 2001-11-22 tuned;
2001-11-22 wenzelm 2001-11-22 thm "point.defs";
2001-11-22 wenzelm 2001-11-22 recovered original "make"; added "fields" operation; renamed "derived_defs" to "defs";
2001-11-22 wenzelm 2001-11-22 renamed "fields" to "flds" (avoid clash with new "fields" operation);
2001-11-21 wenzelm 2001-11-21 locale expressions;
2001-11-21 wenzelm 2001-11-21 use tracing function for trace output;
2001-11-21 wenzelm 2001-11-21 tracing_fn;
2001-11-21 wenzelm 2001-11-21 added tracing, tracing_fn;
2001-11-21 wenzelm 2001-11-21 Set.vimage;
2001-11-21 wenzelm 2001-11-21 got rid of theory Inverse_Image;
2001-11-21 wenzelm 2001-11-21 theory Inverse_Image converted and moved to Set;
2001-11-21 wenzelm 2001-11-21 tuned;
2001-11-20 wenzelm 2001-11-20 tuned;
2001-11-20 wenzelm 2001-11-20 fixed links etc.;
2001-11-20 wenzelm 2001-11-20 * HOL/record: cases/induct for more parts; * syntax: prefer later print_translation functions;
2001-11-20 wenzelm 2001-11-20 prefer later trfuns;
2001-11-20 wenzelm 2001-11-20 moved prefixes1, suffixes1 to library.ML;
2001-11-20 wenzelm 2001-11-20 trfuns *after* binder syntax;
2001-11-20 wenzelm 2001-11-20 added prefixes1, suffixes1;
2001-11-20 wenzelm 2001-11-20 print_depth 10;
2001-11-20 wenzelm 2001-11-20 derive cases/induct rules for ``more'' parts;
2001-11-20 wenzelm 2001-11-20 tuned;
2001-11-20 paulson 2001-11-20 Hyperreal
2001-11-19 wenzelm 2001-11-19 improved treatment of common result name;
2001-11-19 wenzelm 2001-11-19 tuned;
2001-11-19 wenzelm 2001-11-19 multi_theorem: common statement header (covers *all* results);
2001-11-19 wenzelm 2001-11-19 fixed comment; goal: unbind if multiple statements;
2001-11-19 wenzelm 2001-11-19 induct method: localize rews for rule;
2001-11-19 berghofe 2001-11-19 Now handles different theorems with same name more gracefully.
2001-11-19 berghofe 2001-11-19 Improved error message.
2001-11-19 berghofe 2001-11-19 Added setup.
2001-11-19 berghofe 2001-11-19 Moved fastype to Envir.
2001-11-19 berghofe 2001-11-19 Further restructuring of theorem naming functions.
2001-11-19 berghofe 2001-11-19 Added setup for proof rewrite rules.
2001-11-19 berghofe 2001-11-19 - Fixed bug in shrink - Restored old behaviour of thm_proof - Eliminated reference from theory data
2001-11-19 berghofe 2001-11-19 Replaced devar by Envir.head_norm
2001-11-19 berghofe 2001-11-19 Moved head_norm and fastype from unify.ML to envir.ML
2001-11-16 kleing 2001-11-16 fixed maxs bug
2001-11-16 wenzelm 2001-11-16 Ntree and Brouwer converted and moved to ZF/Induct;
2001-11-16 wenzelm 2001-11-16 converted;
2001-11-16 wenzelm 2001-11-16 actually store "coinduct" rule;
2001-11-16 wenzelm 2001-11-16 additional P.marg_comment;
2001-11-16 wenzelm 2001-11-16 \usepackage[latin1]{inputenc};
2001-11-16 paulson 2001-11-16 even more theories from Jacques