*** empty log message ***

List now contains some lexicographic orderings.

added store_tthm;

Improved well-formedness check.

even more tidying of Goal commands

A higher-level treatment of LeadsTo, minimizing use of "reachable"

Simplified proof!!

*** 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.

Deleted obsolete comments.

Adapted to new datatype package.

Script that adapts theories and proof scripts to new datatype package.

make_defs not marked as internal;

late setup of Pure and CPure;

removed global_names flag;

theory_of renamed to theory (and made public);

added Real structure (taken from SML/NJ basis lib);

tuned;

Tidied

Changed "goal" to "Goal"

Updated examples

A little quantifier duplication for IFOL

A few new lemmas by Mark Staples

tuned;

conversion bug in simpproc list_eq

added ex/MonoidGroups (record example); moved Bin and String examples to ex;

added type and update syntax;

added more_update; added type and update syntax;

update -> fun_upd

Map.update -> map_upd, Unpdate.update -> fun_upd Problem: macros get confused about two updates.

added internal;

Adapted to new datatype package.

Adapted to new datatype package.

Renamed '$' to 'Scons' because of clashes with constants of the same name in theories using datatypes.

Added functions addIffs and delIffs which operate on clasimpsets.

Added theorem distinct_lemma (needed for datatypes).

Declaration of type 'nat' as a datatype (this allows usage of exhaust_tac and induct_tac on type 'nat'). Moved some proofs using natE from NatDef.ML to Nat.ML.

Removed nat_case, nat_rec, and natE (now provided by datatype package).