src/HOL/Auth/Yahalom2.ML
changeset 4509 828148415197
parent 4477 b3e5857d8d99
child 4537 4e835bd9fada
     1.1 --- a/src/HOL/Auth/Yahalom2.ML	Fri Jan 02 13:24:53 1998 +0100
     1.2 +++ b/src/HOL/Auth/Yahalom2.ML	Fri Jan 02 17:15:19 1998 +0100
     1.3 @@ -105,11 +105,7 @@
     1.4  (*YM3*)
     1.5  by (blast_tac (claset() addss (simpset())) 2);
     1.6  (*Fake*)
     1.7 -by (best_tac
     1.8 -     (claset() addSDs [impOfSubs (parts_insert_subset_Un RS keysFor_mono)]
     1.9 -               addIs  [impOfSubs analz_subset_parts]
    1.10 -               addDs  [impOfSubs (analz_subset_parts RS keysFor_mono)]
    1.11 -               addss  (simpset())) 1);
    1.12 +by (blast_tac (claset() addSDs [keysFor_parts_insert]) 1);
    1.13  qed_spec_mp "new_keys_not_used";
    1.14  
    1.15  bind_thm ("new_keys_not_analzd",