paulson [Thu, 26 Jun 1997 11:58:05 +0200] rev 3464
Trivial changes in connection with the Yahalom paper.
Changed the order of the premises in no_nonce_YM1_YM2.
Installed B_trusts_YM4_newK using bind_thm.
Improved some comments.
paulson [Mon, 23 Jun 1997 11:33:59 +0200] rev 3459
Removal of structure Context and its replacement by a theorem list of
congruence rules for use in CONTEXT_REWRITE_RULE (where definitions are
processed)