shyps note for prim. rules;

tuned;

tuned current_goals_markers semantics to avoid empty lines;

tidied

auto update

Some more proofs.

added nat_diff_split and a few lemmas in Trancl.

ML_SYSTEM=polyml-3.1;

tuned checklist;

official release;

ML_SYSTEM factory default;

*** empty log message ***

tuned;

records; tuned datatype, inductive, primrec;

*** empty log message ***

Added theorem bool_induct (for rep_datatype).

Added theorem unit_induct (for rep_datatype).

Added theorems True_not_False and False_not_True (for rep_datatype).

unit and bool are now represented as datatypes.

corrected auto_tac (applications of unsafe wrappers)

corrected (and simplified) depth_tac

corrected auto_tac (applications of unsafe wrappers) by correcting (and simplifying) nodup_depth_tac

corrected auto_tac (applications of unsafe wrappers) improved style of several proofs

added SOLVE tactical

tuned;

matharray; records;

SYNC: records (draft version);

Warns when stack is extended; better decl of print_depth

better checking of "defines" in a locale

better reporting of "Additional hypotheses" in a locale

Now users will never see (int 0)

auto update

updated as requested by Markus

export is_ml_identifier;

Updated to new datatype package.

ex/Points added

Example for records

Directory Induct: Added new theory ABexp, removed obsolete theory Simult.

Added new theory ABexp, removed obsolete theory Simult.

Terms are now defined using the new datatype package.

New example for using the datatype package: Arithmetic and boolean expressions.

Removed obsolete theory Simult (see theory Term).

started to add records;

occurs check now handles Bound variables (for soundness)

updated by isatool logo;

tuned block indent;

current_goals_markers;

some additions for Proof General by David Aspinall;

support current_goals_markers ref variable for print_current_goals;

eliminated 'let ... in structure ...' to make SML/NJ 0.93 happy;

fixed index.html;

tuned; record package;

tuned;

standard Blast_tac demos

tidying

locales

Changed interface of inductive.

Changed interface of rep_datatype: Characteristic theorems of datatypes are now specified by xstrings.

Changed interface.

Changed interface of add_inductive: monos and con_defs are now lists of xstrings.

Changed syntax of inductive.

Changed syntax of rep_datatype and inductive: Theorems are no longer specified by a string of ML type "thm list" but by a comma-separated list of identifiers, which are looked up in the theory.

Added theorem prod_induct (needed for rep_datatype).

Changed syntax of rep_datatype.

fixed field_injects;

tuned;

no open;

tuned;

Tutorial

dropped support for SML/NJ 109.x;

field_injects [iffs];

record_split_name;

tuned (all proofs are INSTABLE by David's definition of instability);

improved var names; tuned;

tuned stack_overflow_handler;

made SML/NJ happy;

delSWrapper "record_split_tac";

fixed Syntax module;

split_paired_all.ML;

field types: datatype; record_split_tac; quiet_mode; renamed fst/snd to val/more; structure BasicRecordPackage;

quiet_mode, message;

quiet proofs;

fixed Syntax module;

Datatype instead of Prod;

QUIET_BREADTH_FIRST;

no open; handle multiple trfuns; tuned; removed trfun_names; structure BasicSyntax;

no open; handle multiple trfuns;

no open;

simple Env replaced by Symtab;

added unvarify(T);

Syntax.max_pri;

Symtab.foldl;

quiet_mode, message;

structure Hidden = struct end;

hiding private stuff;

Symtab.foldl;

added foldl, keys;

split_paired_all.ML: turn surjective pairing into split rule;

updated

updated the MLWorks description

another little bug ;-) and minor changes in TLS.*;

little bug ;-)

added keyword 'and'

corrected Header

Addsimps [max_le_iff_conj]; Addsimps [le_min_iff_conj];

changed Super_L and Hyper_R to left and right Meta

layout

solved conflict by taking newest version;

added Clarify_tac to speed up proofs

moved a theorem

fixed comment

fixed some indenting; changed a VERY slow blast_tac to fast_tac

updated, tuned;

added Minho (Portugal);

Fixed bug (improper handling of flag flat_names).

Added quiet_mode flag.

- Changed structure of name spaces - Proofs for datatypes with unneeded parameters are working now - added additional parameter flat_names - added quiet_mode flag

tuned MLWorks options; added print_depth;

MLWorks 2.0;

Changed structure of name spaces for datatypes.