1.1 --- a/src/HOL/Auth/Kerberos_BAN.ML	Thu Aug 20 16:25:32 1998 +0200
     1.2 +++ b/src/HOL/Auth/Kerberos_BAN.ML	Thu Aug 20 16:37:18 1998 +0200
     1.3 @@ -31,13 +31,13 @@
     1.4  \     ==> EX Timestamp K. EX evs: kerberos_ban.    \
     1.5  \            Says B A (Crypt K (Number Timestamp)) \
     1.6  \                 : set evs";
     1.7 +by (cut_facts_tac [SesKeyLife_LB] 1);
     1.8  by (REPEAT (resolve_tac [exI,bexI] 1));
     1.9  by (rtac (kerberos_ban.Nil RS kerberos_ban.Kb1 RS kerberos_ban.Kb2 RS 
    1.10            kerberos_ban.Kb3 RS kerberos_ban.Kb4) 2);
    1.11  by possibility_tac;
    1.12 -by (ALLGOALS (simp_tac (simpset() addsimps [leD]))); (*from NatDef.ML!!!!*)
    1.13 -by (cut_facts_tac [SesKeyLife_LB] 1);
    1.14 -by (trans_tac 1);
    1.15 +by (ALLGOALS Asm_simp_tac);
    1.16 +by (ALLGOALS trans_tac);
    1.17  result();
    1.18  
    1.19