src/HOL/Auth/Event.thy
changeset 17990 86d462f305e0
parent 16417 9bc16273c2d4
child 18570 ffce25f9aa7f
     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";