# HG changeset patch
# User paulson
# Date 844677651 -7200
# Node ID 275ef0f28e1f58f6852678d3466875ca66c17034
# Parent  d08998a11d44517c716183b10daae786feb26b44
Simplified a proof

diff -r d08998a11d44 -r 275ef0f28e1f src/HOL/Auth/Yahalom.ML
--- a/src/HOL/Auth/Yahalom.ML	Mon Oct 07 10:35:47 1996 +0200
+++ b/src/HOL/Auth/Yahalom.ML	Mon Oct 07 10:40:51 1996 +0200
@@ -8,6 +8,8 @@
 From page 257 of
   Burrows, Abadi and Needham.  A Logic of Authentication.
   Proc. Royal Soc. 426 (1989)
+
+DEFINE parts_induct_tac AS IN OtwayRees
 *)
 
 open Yahalom;
@@ -209,7 +211,7 @@
 \        Key K : parts {X} --> Key K : parts (sees lost Spy evs)";
 by (etac yahalom.induct 1);
 by (dtac (YM4_analz_sees_Spy RS synth.Inj) 6);
-by (ALLGOALS (asm_simp_tac (!simpset addsimps pushes)));
+by (ALLGOALS Asm_simp_tac);
 (*Deals with Faked messages*)
 by (EVERY 
     (map (best_tac (!claset addSEs partsEs