Mon, 14 Jul 1997 12:47:21 +0200 Changing "lost" from a parameter of protocol definitions to a constant.
paulson [Mon, 14 Jul 1997 12:47:21 +0200] rev 3519
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.
Mon, 14 Jul 1997 12:44:09 +0200 Fixed delIffs to deal correctly with the D-rule
paulson [Mon, 14 Jul 1997 12:44:09 +0200] rev 3518
Fixed delIffs to deal correctly with the D-rule
Mon, 14 Jul 1997 12:42:28 +0200 Removed redundant addsimps of Un_insert_left, which is now a default simprule
paulson [Mon, 14 Jul 1997 12:42:28 +0200] rev 3517
Removed redundant addsimps of Un_insert_left, which is now a default simprule
Fri, 11 Jul 1997 13:32:39 +0200 Removal of monotonicity reasoning involving "lost" and the theorem
paulson [Fri, 11 Jul 1997 13:32:39 +0200] rev 3516
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.
Fri, 11 Jul 1997 13:30:01 +0200 Now uses the Notes constructor to distinguish the Client (who has chosen M)
paulson [Fri, 11 Jul 1997 13:30:01 +0200] rev 3515
Now uses the Notes constructor to distinguish the Client (who has chosen M) from the Spy (who may have replayed her messages)
Fri, 11 Jul 1997 13:28:53 +0200 Moved some declarations to Message from Public and Shared
paulson [Fri, 11 Jul 1997 13:28:53 +0200] rev 3514
Moved some declarations to Message from Public and Shared
Fri, 11 Jul 1997 13:27:15 +0200 Now loads theory Event, which contains common declarations
paulson [Fri, 11 Jul 1997 13:27:15 +0200] rev 3513
Now loads theory Event, which contains common declarations
Fri, 11 Jul 1997 13:26:15 +0200 Moving common declarations and proofs from theories "Shared"
paulson [Fri, 11 Jul 1997 13:26:15 +0200] rev 3512
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".
Wed, 09 Jul 1997 17:00:34 +0200 removed obsolete init_pps and init_thy_reader;
wenzelm [Wed, 09 Jul 1997 17:00:34 +0200] rev 3511
removed obsolete init_pps and init_thy_reader;
Wed, 09 Jul 1997 16:54:17 +0200 improved type checking errors;
wenzelm [Wed, 09 Jul 1997 16:54:17 +0200] rev 3510
improved type checking errors;
(0) -3000 -1000 -300 -100 -10 +10 +100 +300 +1000 +3000 +10000 +30000 tip