--- a/src/HOL/Auth/Message.ML Wed Sep 25 15:03:13 1996 +0200
+++ b/src/HOL/Auth/Message.ML Wed Sep 25 17:15:18 1996 +0200
@@ -252,6 +252,15 @@
parts_insert_Key, parts_insert_Crypt, parts_insert_MPair];
+goal thy "parts (Key``N) = Key``N";
+by (Auto_tac());
+be parts.induct 1;
+by (Auto_tac());
+qed "parts_image_Key";
+
+Addsimps [parts_image_Key];
+
+
(**** Inductive relation "analz" ****)
val major::prems =
@@ -420,6 +429,15 @@
qed "analz_insert_Crypt_subset";
+goal thy "analz (Key``N) = Key``N";
+by (Auto_tac());
+be analz.induct 1;
+by (Auto_tac());
+qed "analz_image_Key";
+
+Addsimps [analz_image_Key];
+
+
(** Idempotence and transitivity **)
goal thy "!!H. X: analz (analz H) ==> X: analz H";