tidied away duplicate thm
authorpaulson
Wed Oct 26 16:31:53 2005 +0200 (2005-10-26)
changeset 1799086d462f305e0
parent 17989 fa751791be4d
child 17991 ca0958ab3293
tidied away duplicate thm
src/HOL/Auth/Event.thy
src/HOL/Auth/Public.thy
     1.1 --- a/src/HOL/Auth/Event.thy	Tue Oct 25 18:38:21 2005 +0200
     1.2 +++ b/src/HOL/Auth/Event.thy	Wed Oct 26 16:31:53 2005 +0200
     1.3 @@ -90,12 +90,6 @@
     1.4  apply (auto split: event.split) 
     1.5  done
     1.6  
     1.7 -lemma MPair_used [rule_format]:
     1.8 -     "MPair X Y \<in> used evs --> X \<in> used evs & Y \<in> used evs"
     1.9 -apply (induct_tac evs)
    1.10 -apply (auto split: event.split) 
    1.11 -done
    1.12 -
    1.13  
    1.14  subsection{*Function @{term knows}*}
    1.15  
    1.16 @@ -309,7 +303,6 @@
    1.17  
    1.18  val Notes_imp_used = thm "Notes_imp_used";
    1.19  val Says_imp_used = thm "Says_imp_used";
    1.20 -val MPair_used = thm "MPair_used";
    1.21  val Says_imp_knows_Spy = thm "Says_imp_knows_Spy";
    1.22  val Notes_imp_knows_Spy = thm "Notes_imp_knows_Spy";
    1.23  val knows_Spy_partsEs = thms "knows_Spy_partsEs";
     2.1 --- a/src/HOL/Auth/Public.thy	Tue Oct 25 18:38:21 2005 +0200
     2.2 +++ b/src/HOL/Auth/Public.thy	Wed Oct 26 16:31:53 2005 +0200
     2.3 @@ -224,6 +224,8 @@
     2.4  lemma MPair_used_D: "{|X,Y|} \<in> used H ==> X \<in> used H & Y \<in> used H"
     2.5  by (drule used_parts_subset_parts, simp, blast)
     2.6  
     2.7 +text{*There was a similar theorem in Event.thy, so perhaps this one can
     2.8 +  be moved up if proved directly by induction.*}
     2.9  lemma MPair_used [elim!]:
    2.10       "[| {|X,Y|} \<in> used H;
    2.11           [| X \<in> used H; Y \<in> used H |] ==> P |]