src/HOL/Auth/Message.thy
changeset 11230 756c5034f08b
parent 11192 5fd02b905a9a
child 11245 3d9d25a3375b
     1.1 --- a/src/HOL/Auth/Message.thy	Wed Mar 28 13:40:06 2001 +0200
     1.2 +++ b/src/HOL/Auth/Message.thy	Thu Mar 29 10:44:37 2001 +0200
     1.3 @@ -10,10 +10,6 @@
     1.4  theory Message = Main
     1.5  files ("Message_lemmas.ML"):
     1.6  
     1.7 -(*Eliminates a commonly-occurring expression*)
     1.8 -lemma [simp] : "~ (\<forall> x. x\<noteq>y)"
     1.9 -by blast
    1.10 -
    1.11  (*Needed occasionally with spy_analz_tac, e.g. in analz_insert_Key_newK*)
    1.12  lemma [simp] : "A Un (B Un A) = B Un A"
    1.13  by blast
    1.14 @@ -31,8 +27,8 @@
    1.15      that of a public key is the private key and vice versa*)
    1.16  
    1.17  constdefs
    1.18 -  isSymKey :: "key=>bool"
    1.19 -  "isSymKey K == (invKey K = K)"
    1.20 +  symKeys :: "key set"
    1.21 +  "symKeys == {K. invKey K = K}"
    1.22  
    1.23  datatype  (*We allow any number of friendly agents*)
    1.24    agent = Server | Friend nat | Spy