src/HOL/Auth/Message.ML
changeset 3583 5a47b869d16a
parent 3519 ab0a9fbed4c0
child 3650 282ffdc91884
equal deleted inserted replaced
3582:b87c86b6c291 3583:5a47b869d16a
   522           ORELSE' etac equalityE));
   522           ORELSE' etac equalityE));
   523 qed "analz_cong";
   523 qed "analz_cong";
   524 
   524 
   525 
   525 
   526 goal thy "!!H. analz H = analz H' ==> analz(insert X H) = analz(insert X H')";
   526 goal thy "!!H. analz H = analz H' ==> analz(insert X H) = analz(insert X H')";
   527 by (asm_simp_tac (!simpset addsimps [insert_def] 
   527 by (asm_simp_tac (!simpset addsimps [insert_def] delsimps [singleton_conv]
   528                            setloop (rtac analz_cong)) 1);
   528                            setloop (rtac analz_cong)) 1);
   529 qed "analz_insert_cong";
   529 qed "analz_insert_cong";
   530 
   530 
   531 (*If there are no pairs or encryptions then analz does nothing*)
   531 (*If there are no pairs or encryptions then analz does nothing*)
   532 goal thy "!!H. [| ALL X Y. {|X,Y|} ~: H;  ALL X K. Crypt K X ~: H |] ==> \
   532 goal thy "!!H. [| ALL X Y. {|X,Y|} ~: H;  ALL X K. Crypt K X ~: H |] ==> \