# HG changeset patch
# User paulson
# Date 997096326 -7200
# Node ID 96b5b27da55ca1038f6dfe48f18318914aabd2af
# Parent  cf3e7f5ad0e1d0e98fe0fef741ea85fc44d9c1b3
three new theorems

diff -r cf3e7f5ad0e1 -r 96b5b27da55c src/HOL/Auth/Event.thy
--- 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 = {*