*** empty log message ***

Lemma renamed in HOL.

Added macro `termi'

New lemmas in List and Lambda in IsaMakefile

Removed duplicate thms (see comment to Arith.ML)

Removed duplicate thms: less_imp_add_less = trans_less_add1 le_imp_add_le = trans_le_add1

Removed comments.

even more tidying of Goal commands

disjointness

Now recognizes both {}= and ={}

Disjointness reasoning by AddEs [equals0E, sym RS equals0E] and consequential changes (and tidying)

New result from AC directory

added solve_tac;

New results from AC

First steps towards termination of simply typed terms.

binding / skolem vars;

Null program and a few new results

Finished the example

Indentation, comments

Renamed equals0D to equals0E

Tidied

Removal of "disjoint" translation

New record type of programs

Union primitives and examples

tuned; Display.print_goals function moved to Locale.print_goals;

added LocaleGroup, PiSets examples;

added Open_locale, Close_locale; thm(s): use Locale.get_thm(s);

added 'locale' section;

Locale.setup;

added export: thm -> thm; exported print_current_goals_default; locale support;

moved print_goals to locale.ML;

added locale.ML;

added icons;

Renamed equals0D to equals0E

Renamed equals0D to equals0E; tidied

Constant "invariant" and new constrains_tac, ensures_tac

Tidying

Boolean quantification

Deleted the redundant rule mem_if

fixed disjount translation;

tuned comments;

Better comments

New rewrite rules for quantification over bounded UNIONs

Tidied; uses records

new theorems for partial funcs

Pretty.sym;

size / length: printable length;

isatool expandshort;

Removal of obsolete "open" commands from heads of .ML files

Replaced nat.exhaustion by nat.exhaust

Removed HOL/IMP/Com.ML because it contained only an "open" declaration

tidied

Removal of obsolete "open" commands from heads of .ML files

Fixed primrec.

Fixed primrec.

made SML/NJ happy;

functorized Clasimp module;

fixed primrec;

tuned;

Equations are now stored in theory.