Tidied Key_supply3
authorpaulson
Wed Nov 05 13:27:29 1997 +0100 (1997-11-05)
changeset 415631251763848d
parent 4155 53f60f51333c
child 4157 200f897f0858
Tidied Key_supply3
src/HOL/Auth/Shared.ML
     1.1 --- a/src/HOL/Auth/Shared.ML	Wed Nov 05 13:26:19 1997 +0100
     1.2 +++ b/src/HOL/Auth/Shared.ML	Wed Nov 05 13:27:29 1997 +0100
     1.3 @@ -175,14 +175,13 @@
     1.4  \                      Key K'' ~: used evs'' & K ~= K' & K' ~= K'' & K ~= K''";
     1.5  by (cut_inst_tac [("evs","evs")] (Finites.emptyI RS Key_supply_ax) 1);
     1.6  by (etac exE 1);
     1.7 -by (cut_inst_tac [("evs","evs'")] 
     1.8 +(*Blast_tac requires instantiation of the keys for some reason*)
     1.9 +by (cut_inst_tac [("evs","evs'"), ("a1","K")] 
    1.10      (Finites.emptyI RS Finites.insertI RS Key_supply_ax) 1);
    1.11  by (etac exE 1);
    1.12 -by (cut_inst_tac [("evs","evs''")] 
    1.13 +by (cut_inst_tac [("evs","evs''"), ("a1","Ka"), ("a2","K")] 
    1.14      (Finites.emptyI RS Finites.insertI RS Finites.insertI RS Key_supply_ax) 1);
    1.15 -by (Clarify_tac 1);
    1.16 -by (Full_simp_tac 1);
    1.17 -by (fast_tac (claset() addSEs [allE]) 1);
    1.18 +by (Blast_tac 1);
    1.19  qed "Key_supply3";
    1.20  
    1.21  goal thy "Key (@ K. Key K ~: used evs) ~: used evs";