# HG changeset patch
# User paulson
# Date 1130337113 -7200
# Node ID 86d462f305e0920630ae38d572d2339fd920dcac
# Parent  fa751791be4d1461c9921751b46a9ffe2af86fed
tidied away duplicate thm

diff -r fa751791be4d -r 86d462f305e0 src/HOL/Auth/Event.thy
--- 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";
diff -r fa751791be4d -r 86d462f305e0 src/HOL/Auth/Public.thy
--- 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 |]