Simplified a proof
authorpaulson
Mon Oct 07 10:40:51 1996 +0200 (1996-10-07)
changeset 2060275ef0f28e1f
parent 2059 d08998a11d44
child 2061 b14a08bf61bf
Simplified a proof
src/HOL/Auth/Yahalom.ML
     1.1 --- a/src/HOL/Auth/Yahalom.ML	Mon Oct 07 10:35:47 1996 +0200
     1.2 +++ b/src/HOL/Auth/Yahalom.ML	Mon Oct 07 10:40:51 1996 +0200
     1.3 @@ -8,6 +8,8 @@
     1.4  From page 257 of
     1.5    Burrows, Abadi and Needham.  A Logic of Authentication.
     1.6    Proc. Royal Soc. 426 (1989)
     1.7 +
     1.8 +DEFINE parts_induct_tac AS IN OtwayRees
     1.9  *)
    1.10  
    1.11  open Yahalom;
    1.12 @@ -209,7 +211,7 @@
    1.13  \        Key K : parts {X} --> Key K : parts (sees lost Spy evs)";
    1.14  by (etac yahalom.induct 1);
    1.15  by (dtac (YM4_analz_sees_Spy RS synth.Inj) 6);
    1.16 -by (ALLGOALS (asm_simp_tac (!simpset addsimps pushes)));
    1.17 +by (ALLGOALS Asm_simp_tac);
    1.18  (*Deals with Faked messages*)
    1.19  by (EVERY 
    1.20      (map (best_tac (!claset addSEs partsEs