--- a/src/HOL/Auth/Message.ML Fri Jun 19 11:14:20 1998 +0200
+++ b/src/HOL/Auth/Message.ML Fri Jun 19 11:20:36 1998 +0200
@@ -464,7 +464,7 @@
(*Case analysis: either the message is secure, or it is not!
Effective, but can cause subgoals to blow up!
- Use with expand_if; apparently split_tac does not cope with patterns
+ Use with split_if; apparently split_tac does not cope with patterns
such as "analz (insert (Crypt K X) H)" *)
goal thy "analz (insert (Crypt K X) H) = \
\ (if (Key (invKey K) : analz H) \