--- a/src/HOL/Auth/Kerberos_BAN.ML Tue Apr 18 15:56:41 2000 +0200
+++ b/src/HOL/Auth/Kerberos_BAN.ML Wed Apr 19 11:09:59 2000 +0200
@@ -239,8 +239,9 @@
by (etac kerberos_ban.induct 1);
by analz_spies_tac;
by (ALLGOALS
- (asm_simp_tac (simpset() addsimps [analz_insert_eq, analz_insert_freshK]
- @ pushes)));
+ (asm_simp_tac (simpset() addsimps [less_SucI, analz_insert_eq,
+ analz_insert_freshK]
+ @ pushes)));
(*Oops*)
by (blast_tac (claset() addDs [unique_session_keys] addIs [less_SucI]) 4);
(*Kb2*)