src/HOL/Auth/TLS.ML
changeset 3919 c036caebfc75
parent 3772 6ee707a73248
child 3961 6a8996fb7d99
     1.1 --- a/src/HOL/Auth/TLS.ML	Fri Oct 17 15:23:14 1997 +0200
     1.2 +++ b/src/HOL/Auth/TLS.ML	Fri Oct 17 15:25:12 1997 +0200
     1.3 @@ -146,7 +146,7 @@
     1.4      REPEAT (FIRSTGOAL analz_mono_contra_tac)
     1.5      THEN 
     1.6      fast_tac (!claset addss (!simpset)) i THEN
     1.7 -    ALLGOALS (asm_simp_tac (!simpset setloop split_tac [expand_if]));
     1.8 +    ALLGOALS (asm_simp_tac (!simpset addsplits [expand_if]));
     1.9  
    1.10  
    1.11  (** Theorems of the form X ~: parts (spies evs) imply that NOBODY
    1.12 @@ -198,13 +198,13 @@
    1.13      ClientKeyExch_tac  (i+6)  THEN	(*ClientKeyExch*)
    1.14      ALLGOALS (asm_simp_tac 
    1.15                (!simpset addcongs [if_weak_cong]
    1.16 -                        setloop split_tac [expand_if]))  THEN
    1.17 +                        addsplits [expand_if]))  THEN
    1.18      (*Remove instances of pubK B:  the Spy already knows all public keys.
    1.19        Combining the two simplifier calls makes them run extremely slowly.*)
    1.20      ALLGOALS (asm_simp_tac 
    1.21                (!simpset addcongs [if_weak_cong]
    1.22  			addsimps [insert_absorb]
    1.23 -                        setloop split_tac [expand_if]));
    1.24 +                        addsplits [expand_if]));
    1.25  
    1.26  
    1.27  (*** Properties of items found in Notes ***)