--- a/src/HOL/Auth/Event.thy Mon Aug 06 12:46:21 2001 +0200
+++ b/src/HOL/Auth/Event.thy Mon Aug 06 13:12:06 2001 +0200
@@ -79,6 +79,22 @@
| Notes A X => parts {X} Un (used evs))"
+lemma Notes_imp_used [rule_format]: "Notes A X : set evs --> X : used evs"
+apply (induct_tac evs);
+apply (auto split: event.split)
+done
+
+lemma Says_imp_used [rule_format]: "Says A B X : set evs --> X : used evs"
+apply (induct_tac evs);
+apply (auto split: event.split)
+done
+
+lemma MPair_used [rule_format]:
+ "MPair X Y : used evs --> X : used evs & Y : used evs"
+apply (induct_tac evs);
+apply (auto split: event.split)
+done
+
use "Event_lemmas.ML"
method_setup analz_mono_contra = {*