Useful new lemma

--- a/src/HOL/Auth/Message.ML	Fri Jun 06 21:49:47 1997 +0200
+++ b/src/HOL/Auth/Message.ML	Mon Jun 09 10:21:05 1997 +0200
@@ -477,6 +477,10 @@
    "!!H. Y: analz (insert X H) ==> X: analz H --> Y: analz H"
 *)
 
+goal thy "!!H. X: analz H ==> analz (insert X H) = analz H";
+by (blast_tac (!claset addIs [analz_cut, analz_insertI]) 1);
+qed "analz_insert_eq";
+
 
 (** A congruence rule for "analz" **)