src/HOL/Metis_Examples/Message.thy

                analz (insert (Crypt K X) H) =
                insert (Crypt K X) (analz (insert X H))"
 by (intro equalityI lemma1 lemma2)
 
 text{*Case analysis: either the message is secure, or it is not! Effective,
-but can cause subgoals to blow up! Use with @{text "split_if"}; apparently
+but can cause subgoals to blow up! Use with @{text "if_split"}; apparently
 @{text "split_tac"} does not cope with patterns such as @{term"analz (insert
 (Crypt K X) H)"} *}
 lemma analz_Crypt_if [simp]:
      "analz (insert (Crypt K X) H) =
           (if (Key (invKey K) \<in> analz H)