src/HOL/Auth/TLS.ML
changeset 6915 4ab8e31a8421
parent 6308 76f3865a2b1d
child 7057 b9ddbb925939
equal deleted inserted replaced
6914:ad689270a265 6915:4ab8e31a8421
   174     THEN' hyp_subst_tac;
   174     THEN' hyp_subst_tac;
   175 
   175 
   176 fun analz_induct_tac i = 
   176 fun analz_induct_tac i = 
   177     etac tls.induct i   THEN
   177     etac tls.induct i   THEN
   178     ClientKeyExch_tac  (i+6)  THEN	(*ClientKeyExch*)
   178     ClientKeyExch_tac  (i+6)  THEN	(*ClientKeyExch*)
   179     ALLGOALS (asm_simp_tac 
   179     ALLGOALS (asm_simp_tac (simpset() addsimps split_ifs @ pushes))  THEN
   180               (simpset() addcongs [if_weak_cong]
       
   181                          addsimps split_ifs @ pushes))  THEN
       
   182     (*Remove instances of pubK B:  the Spy already knows all public keys.
   180     (*Remove instances of pubK B:  the Spy already knows all public keys.
   183       Combining the two simplifier calls makes them run extremely slowly.*)
   181       Combining the two simplifier calls makes them run extremely slowly.*)
   184     ALLGOALS (asm_simp_tac 
   182     ALLGOALS (asm_simp_tac (simpset() addsimps [insert_absorb]));
   185               (simpset() addcongs [if_weak_cong]
       
   186 			 addsimps [insert_absorb]));
       
   187 
   183 
   188 
   184 
   189 (*** Properties of items found in Notes ***)
   185 (*** Properties of items found in Notes ***)
   190 
   186 
   191 Goal "[| Notes A {|Agent B, X|} : set evs;  evs : tls |]  \
   187 Goal "[| Notes A {|Agent B, X|} : set evs;  evs : tls |]  \