src/HOL/Auth/Yahalom.ML
changeset 3919 c036caebfc75
parent 3708 56facaebf3e3
child 3961 6a8996fb7d99
     1.1 --- a/src/HOL/Auth/Yahalom.ML	Fri Oct 17 15:23:14 1997 +0200
     1.2 +++ b/src/HOL/Auth/Yahalom.ML	Fri Oct 17 15:25:12 1997 +0200
     1.3 @@ -227,7 +227,7 @@
     1.4  by (ALLGOALS
     1.5      (asm_simp_tac 
     1.6       (!simpset addsimps [analz_insert_eq, analz_insert_freshK]
     1.7 -               setloop split_tac [expand_if])));
     1.8 +               addsplits [expand_if])));
     1.9  (*Oops*)
    1.10  by (blast_tac (!claset addDs [unique_session_keys]) 3);
    1.11  (*YM3*)
    1.12 @@ -499,7 +499,7 @@
    1.13  by (ALLGOALS
    1.14      (asm_simp_tac 
    1.15       (!simpset addsimps [analz_insert_eq, analz_insert_freshK]
    1.16 -               setloop split_tac [expand_if])));
    1.17 +               addsplits [expand_if])));
    1.18  (*Prove YM3 by showing that no NB can also be an NA*)
    1.19  by (blast_tac (!claset addDs [Says_imp_spies RS parts.Inj]
    1.20  	               addSEs [MPair_parts]