Some streamlining of text. Theory library is now assumed to be LOCAL and not at TUM.

tuned;

tuned width of pics;

tuned;

oops;

tuned pics;

made weblint happy;

oops;

Id;

tuned; fixed links;

tuned;

main Isabelle page;

New example

Domain r, Range r replace fst``r, snd``r

increased precedence of unary minus from 80 to 100 requires a similar increase for %# and %%#

increased precedence of unary minus from 80 to 100

Charpentier laws

the Increasing operator

no need for int_0

locales now implicitly quantify over free variables

tuned current_goals_markers;

Moved "instance set:...{power} from Set.thy to RelPow.thy, where is is needed

Explicit (and improved) simprules for binary arithmetic. New default simprules to eliminate (int 0) and (z + - w)

*** empty log message ***

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;