tuned;

make SML/NJ happy;

added Pure/Isar/rule_context.ML;

gcd_dvd1 and gcd_dvd2 proven simultaneously;

moved lemmas to theory Hilbert_Choice;

tuned; meson lemmas from Tools/meson.ML;

added remdups_rl;

clarified order of merge_lists';

clarified order in gen_merge_lists';

fixed SML/NJ error (!?);

use merge_lists, merge_alists;

Symtab.merge_multi'; tuned;

type variables: clarified "used" vs. "occ";

Library.gen_merge_lists';

clarified locale operations (rename, merge); tuned;

print_locale: expr;

added join, merge_multi('); tuned extend, make, merge;

merge_stamps: merge_lists' with reversed args;

gen_merge_lists;

added gen_merge_lists(') and merge_lists('); removed obsolete generic_extend, generic_merge, extend_list;

gen_merge_lists';

generic_merge;

converted simp lemmas;

tuned;

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

finish_global: Drule.strip_shyps_warning (just for warning);

ext_tsig_classes: rebuild_tsig!!!!!

local_standard: plain strip_shyps instead of strip_shyps_warning;

last-minute tidying

updated;

GPLed;

write_keywords: string argument (logic name);

isatool unsymbolize;

Modified to make the files build with the new changes in ZF

depends on Epsilon!

fix_frees: rev;

prove: raise ERROR_MESSAGE;

updated;

* ZF: new-style theory commands '(co)inductive', '(co)datatype', 'rep_datatype', 'inductive_cases'; also methods 'ind_cases', 'induct_tac', 'case_tac', and 'typecheck' (with attribute 'TC');

type_solver_tac: use TCSET' to refer to context of goal state (does *not* work with local proof contexts of Isar / new-style locales);

setup DatatypeTactics.setup;

added Induct/Binary_Trees.thy, Induct/Tree_Forest (converted from former ex/TF.ML ex/TF.thy ex/Term.ML ex/Term.thy);

no handle ERROR;

fixed;

Isar version of 'rep_datatype';

avoid handle _;

added TCSET(') tacticals;

added Term and Tree_Forest (from converted ZF/ex);

TF and Term moved to ZF/Induct;

miniscoping of UN and INT

Added new entry

New files

new theories from Jacques Fleuriot

*** empty log message ***

converted datatype examples moved from ZF/ex to ZF/Induct;

document setup;

removed BT, Data, Enum (see ZF/Induct);

case_names;

added Datatypes, Binary_Trees (from ZF/ex);

Isar attribute and method setup;

fix path prefix;

use proper intr_names (for required case_names); store con_defs, case_eqns, recursor_eqns, free_iffs, free_elims;

added Induct/Binary_Trees.thy, Induct/Datatypes.thy; removed ex/Data.ML ex/Data.thy ex/Enum.ML ex/Enum.thy;

tuned;

updated;