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)