--- a/src/HOL/Auth/Event.thy Tue Oct 25 18:38:21 2005 +0200
+++ b/src/HOL/Auth/Event.thy Wed Oct 26 16:31:53 2005 +0200
@@ -90,12 +90,6 @@
apply (auto split: event.split)
done
-lemma MPair_used [rule_format]:
- "MPair X Y \<in> used evs --> X \<in> used evs & Y \<in> used evs"
-apply (induct_tac evs)
-apply (auto split: event.split)
-done
-
subsection{*Function @{term knows}*}
@@ -309,7 +303,6 @@
val Notes_imp_used = thm "Notes_imp_used";
val Says_imp_used = thm "Says_imp_used";
-val MPair_used = thm "MPair_used";
val Says_imp_knows_Spy = thm "Says_imp_knows_Spy";
val Notes_imp_knows_Spy = thm "Notes_imp_knows_Spy";
val knows_Spy_partsEs = thms "knows_Spy_partsEs";
--- a/src/HOL/Auth/Public.thy Tue Oct 25 18:38:21 2005 +0200
+++ b/src/HOL/Auth/Public.thy Wed Oct 26 16:31:53 2005 +0200
@@ -224,6 +224,8 @@
lemma MPair_used_D: "{|X,Y|} \<in> used H ==> X \<in> used H & Y \<in> used H"
by (drule used_parts_subset_parts, simp, blast)
+text{*There was a similar theorem in Event.thy, so perhaps this one can
+ be moved up if proved directly by induction.*}
lemma MPair_used [elim!]:
"[| {|X,Y|} \<in> used H;
[| X \<in> used H; Y \<in> used H |] ==> P |]