New theory of the inverse image of a function

Added some lemmas.

Catches bad elim rules, handling exception OPTION

New laws for union

New laws for id

New induction schemas for lists (length and snoc).

*** empty log message ***

Congruence rules use == in premises now.

Congruence rules use == in premises now. New class linord.

minor improvements

re-arranged bindings for many function keys

extended input syntax to handle names of special keys

moved Ctrl entry before Alt entry extended input syntax to handle names of special keys

New theorem eq_imp_le

Four new Union/Intersection laws

corrected problem with auto_tac: now uses a variant of depth_tac that avoids interference of the simplifier with dup_step_tac

added New Jersey mirror;

Improved loop-test for rewrite rules a little. Should be done properly!

tuned comment;

added append (curried);

*** empty log message ***

Sign.merge vs. Sign.nontriv_merge;

tuned comments;

oops;

tuned print_cs;

updated;

tuned;

added explicit signature; improved comments;

improved comments;

fixed add_trrules: intern root;

export map_trrule;

tuned add_trrules;

improved is_letter etc.;

New Addsimps for Compl rules

New AddIffs le_0_eq and neq0_conv

Replaced ALLNEWSUBGOALS by THEN_ALL_NEW

Used THEN_ALL_NEW.

moved freeze_thaw to drule.ML

Tidying; rotate_prems; moved freeze_thaw from tactic.ML

AC and other rewrite rules for Un and Int

auto update

Added reference to rotate_prems

filter_size -> length_filter

Added `remdups' nodup -> nodups

added Vartab: TABLE;

added param;

added THEN_ALL_NEW;

New theorem Image_id

New theorem order_eq_refl

New max, min theorems

Added some more explicit guarantees of key secrecy for agents Deleted spurious A~=Spy assumptions

Fixed a lot of overfull and underfull lines (hboxes)

Updated the description of how to set up hyp_subst_tac

New example, Pow_Sigma_bij

fixed WWW links

Three new facts about Image

Replaced \\1 by $1 as Perl itself asked me to...

Fixed the description of recdef

tuned msgs;

improved tracing of rewrite rule application;

removed dead messy code;

added read_var;

tuned;

Updated MOD reference

added symbols syntax;

reorganized into individual theories;

tuned;

make images;

tuned URL;

polyml-3.1;

obsolete;

added thms wrt weakening and strengthening in Abstraction;

New Jersey inactive;

HOL/record;

error with instantiantion of sub-records removed

added record.ML;

tuned;

added unit and prod stuff;

fixed Id;

smlnj-110 factory default;

added of_sort;

added base_path;

added simulations files to IOA;

added forward simulation correectness;

Simplification: sel make and update make

added abstraction files;

added further IOA liles;

updated to Isabelle98;

tuned;

added files containing temproal logic and abstraction;

Delsimprocs nat_cancel;

tuned;

Tidying, mostly to do with handling a more specific version of Fake_parts_insert

tuned;

tuned;

fixed author;

Simplified proofs by omitting PA = {|XA, ...|} from RA2

trivial tidy

tuned;

automatic index.html patch;

tuned;

tuned ISABELLE_TMP_PREFIX;

thm_ord;

eliminated make_ord;

ISABELLE_TMP_PREFIX: $LOGNAME

several minor updates;

tuned;

index.html for Isabelle Distribution Area;

updated to Isabelle98;

tuned;

fixed thm_less;

Expressed most Oops rules using Notes instead of Says, and other tidying