src/HOL/Auth/OtwayRees_AN.ML
changeset 2891 d8f254ad1ab9
parent 2837 dee1c7f1f576
child 3102 4d01cdc119d2
     1.1 --- a/src/HOL/Auth/OtwayRees_AN.ML	Fri Apr 04 11:18:19 1997 +0200
     1.2 +++ b/src/HOL/Auth/OtwayRees_AN.ML	Fri Apr 04 11:18:52 1997 +0200
     1.3 @@ -311,7 +311,7 @@
     1.4  \           A ~: lost;  B ~: lost;  evs : otway lost |]             \
     1.5  \        ==> Key K ~: analz (sees lost Spy evs)";
     1.6  by (forward_tac [Says_Server_message_form] 1 THEN assume_tac 1);
     1.7 -by (fast_tac (!claset addSEs [lemma]) 1);
     1.8 +by (blast_tac (!claset addSEs [lemma]) 1);
     1.9  qed "Spy_not_see_encrypted_key";
    1.10  
    1.11  
    1.12 @@ -327,7 +327,7 @@
    1.13  by (rtac (subset_insertI RS sees_mono RS analz_mono RS contra_subsetD) 1);
    1.14  by (rtac (sees_lost_agent_subset_sees_Spy RS analz_mono RS contra_subsetD) 1);
    1.15  by (FIRSTGOAL (rtac Spy_not_see_encrypted_key));
    1.16 -by (REPEAT_FIRST (fast_tac (!claset addIs [otway_mono RS subsetD])));
    1.17 +by (REPEAT_FIRST (blast_tac (!claset addIs [otway_mono RS subsetD])));
    1.18  qed "Agent_not_see_encrypted_key";
    1.19  
    1.20