changeset 13926 | 6e62e5357a10 |
parent 13630 | a013a9dd370f |
--- a/src/HOL/Auth/KerberosIV.ML Sat Apr 26 12:38:17 2003 +0200 +++ b/src/HOL/Auth/KerberosIV.ML Sat Apr 26 12:38:42 2003 +0200 @@ -177,7 +177,7 @@ \ Key K \\<notin> used evs --> K \\<notin> keysFor (parts (spies evs))"; by (parts_induct_tac 1); (*Fake*) -by (blast_tac (claset() addSDs [keysFor_parts_insert]) 1); +by (force_tac (claset() addSDs [keysFor_parts_insert], simpset()) 1); (*Others*) by (ALLGOALS Blast_tac); qed_spec_mp "new_keys_not_used";