Extended match_proof to handle abstractions.

tuned;

improved ordering of evaluated elements;

time_use_thy "Locales";

Isar conversion

theory Locales temporarily disabled;

beginnings of actual locale expressions;

improved locale expression syntax;

locale expression import;

import locale expression;

tuned;

added uname; syntax for locale expressions (presently unused);

tuned;

thm "point.defs";

recovered original "make"; added "fields" operation; renamed "derived_defs" to "defs";

renamed "fields" to "flds" (avoid clash with new "fields" operation);

locale expressions;

use tracing function for trace output;

tracing_fn;

added tracing, tracing_fn;

Set.vimage;

got rid of theory Inverse_Image;

theory Inverse_Image converted and moved to Set;

tuned;

tuned;

fixed links etc.;

* HOL/record: cases/induct for more parts; * syntax: prefer later print_translation functions;

prefer later trfuns;

moved prefixes1, suffixes1 to library.ML;

trfuns *after* binder syntax;

added prefixes1, suffixes1;

print_depth 10;

derive cases/induct rules for ``more'' parts;

tuned;

Hyperreal

improved treatment of common result name;

tuned;

multi_theorem: common statement header (covers *all* results);

fixed comment; goal: unbind if multiple statements;

induct method: localize rews for rule;

Now handles different theorems with same name more gracefully.

Improved error message.

Added setup.

Moved fastype to Envir.

Further restructuring of theorem naming functions.

Added setup for proof rewrite rules.

- Fixed bug in shrink - Restored old behaviour of thm_proof - Eliminated reference from theory data

Replaced devar by Envir.head_norm

Moved head_norm and fastype from unify.ML to envir.ML

fixed maxs bug

Ntree and Brouwer converted and moved to ZF/Induct;

converted;

actually store "coinduct" rule;

additional P.marg_comment;

\usepackage[latin1]{inputenc};

even more theories from Jacques