# HG changeset patch
# User paulson
# Date 865844465 -7200
# Node ID 05b397185e1d66ed91aab0c93b399069a8734eff
# Parent  d21b920363abfb038d504c1a0367715d64a51efc
Useful new lemma

diff -r d21b920363ab -r 05b397185e1d src/HOL/Auth/Message.ML
--- 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" **)