Added function `replicate' and lemmas map_cong and set_replicate.

cleaned up; added getenv;

Corrected a comment

Added a take/dropWhile lemma.

Generalized nth_drop (Conny).

Corected bug in def of dropWhile (also present in Haskell lib!)

Had to remove {x.x=a} = a from !simpset in one proof.

Added {x.x=a} = a to !simpset.

removed split_paired_Ex; fixed proc args;

new simproc

*** empty log message ***

load simplifier.ML (again);

added prems argument to simplification procedures;

remove references to simplifier.ML;

improved rewrite_thm / rewrite_goals to handle conditional eqns;

Added a few lemmas.

Deleted comment.

Replaced clumsy rewriting by the new function simplify on thms.

List.ML: added lemmas by Stefan Merz. simpodata.ML: removed rules about ? now subsumed by simplification proc.

set_of_list -> set

Simplified a few proofs because of improved simplification.

Prod.ML: Added split_paired_EX and lots of comments about failed attempts to automate reasoning about products. simpdata.ML: added simplification procedure for simplifying existential statements of the form ? x. ... & x = t & ...

added simplification meta rules;

standard congs;

Now rename_params_rule merely issues warnings--and does nothing--if the renaming cannot be performed. Previously it raised a fatal error.

Now Datatype.occs_in_prems prints the necessary warning ITSELF. It is also easier to invoke and even works if the induction variable is a parameter (rather than a free variable).

Uses new version of Datatype.occs_in_prems

auto update

Removal of tactical STATE

fixed polymorphic val;

tuned congs: standard;

improved simp tracing;

added simplification meta rules;

tmp fix to accomodate rep_ss changes;

added rewrite_thm;

tuned apsome;

added error_msg;

tuned error / warning;

added print_ss; improved merge;

added dest_mss, merge_mss; fixed matching of simproc lhss;

tuned title;

added dest and merge operations;

added pretty_cterm;

improved print_cs;

Cosmetic changes: margins, indentation, ...

Now possibility_tac is an explicit function, in order to delay the evaluation of \!simpset

Cosmetic changes: margins, indentation, ...

Now possibility_tac and basic_possibility_tac are explicit functions, in order to delay the evaluation of \!simpset

Deleted the superfluous assumption A ~= B, which must hold anyway by induction

Fixed the spelling of AUTH_NAMES--it could not have worked before\!

Option is a synonym for General because MLWorks does not yet provide Option as a separate structure

Removal of the tactical STATE

Removal of the tactical STATE

tuned error propagation msg;

defs may now be conditional; improved output of warnings / errors;

renamed |-> <-| <-> to Parse/PrintRule;

tuned warning;

tuned warnings; print_current_goals_fn, result_error_fn hooks replace print_goals_ref;

considered removal of print_goals_ref;

defs: allow conditions;

tuned warning; improved comments;

renamed |-> <-| <-> to Parse/PrintRule;

tuned warning;

tuned warning; renamed |-> <-| <-> to Parse/PrintRule;

improved output channels: normal, warning, error;

fixed EqI meta rule;

changes needed for introducing fairness

changes neede for introducing fairness

changes needed for adding fairness

fixed merge of internal simprocs;

Changing "lost" from a parameter of protocol definitions to a constant. Advantages: no "lost" argument everywhere; fewer Vars in subgoals; less need for specially instantiated rules Disadvantage: can no longer prove "Agent_not_see_encrypted_key", but this theorem was never used, and its original proof was also broken the introduction of the "Notes" constructor.

Fixed delIffs to deal correctly with the D-rule

Removed redundant addsimps of Un_insert_left, which is now a default simprule

Removal of monotonicity reasoning involving "lost" and the theorem Agent_not_see_encrypted_key, which (a) is never used and (b) becomes harder to prove when Notes is available.

Now uses the Notes constructor to distinguish the Client (who has chosen M) from the Spy (who may have replayed her messages)

Moved some declarations to Message from Public and Shared

Now loads theory Event, which contains common declarations

Moving common declarations and proofs from theories "Shared" and "Public" to "Event". NB the original "Event" theory was later renamed "Shared". Addition of the Notes constructor to datatype "event".

removed obsolete init_pps and init_thy_reader;

improved type checking errors;

removed init_pps;

removed init_database;

Improved length = size translation.

New proofs involving CERTIFICATE VERIFY

eliminated chmod -w;

-w option;

NOWRITE;

added -w option;

Changed some variables of type msg to lower case (e.g. from NB to nb

New constant "certificate"--just an abbreviation

Reduced priority of postfix ^* etc operators such that they are the same as application. Eg wf r^* now needs to be written wf(r^*).

Automatic update

Now catches the error of calling tgoalw when there are no goals to prove, instead of just letting USyntax.list_mk_conj raise an exception

Simplified the new proofs about division

New comments on how to deal with unproved termination conditions

Fixed comments