# HG changeset patch
# User paulson
# Date 903623838 -7200
# Node ID a32312d17ed646087406ef6d3d622fd85e403514
# Parent  6d6467c2b8b9667c28b7fd88c0facd743cf3d507
tidied

diff -r 6d6467c2b8b9 -r a32312d17ed6 src/HOL/Auth/Kerberos_BAN.ML
--- a/src/HOL/Auth/Kerberos_BAN.ML	Thu Aug 20 16:25:32 1998 +0200
+++ b/src/HOL/Auth/Kerberos_BAN.ML	Thu Aug 20 16:37:18 1998 +0200
@@ -31,13 +31,13 @@
 \     ==> EX Timestamp K. EX evs: kerberos_ban.    \
 \            Says B A (Crypt K (Number Timestamp)) \
 \                 : set evs";
+by (cut_facts_tac [SesKeyLife_LB] 1);
 by (REPEAT (resolve_tac [exI,bexI] 1));
 by (rtac (kerberos_ban.Nil RS kerberos_ban.Kb1 RS kerberos_ban.Kb2 RS 
           kerberos_ban.Kb3 RS kerberos_ban.Kb4) 2);
 by possibility_tac;
-by (ALLGOALS (simp_tac (simpset() addsimps [leD]))); (*from NatDef.ML!!!!*)
-by (cut_facts_tac [SesKeyLife_LB] 1);
-by (trans_tac 1);
+by (ALLGOALS Asm_simp_tac);
+by (ALLGOALS trans_tac);
 result();