--- a/src/Doc/Tutorial/Protocol/Message.thy Tue Feb 23 16:41:14 2016 +0100
+++ b/src/Doc/Tutorial/Protocol/Message.thy Tue Feb 23 17:47:23 2016 +0100
@@ -483,7 +483,7 @@
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]:
@@ -918,4 +918,4 @@
end
-(*>*)
\ No newline at end of file
+(*>*)