made more generic;

Shortened names and added new thm.

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;