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 |]