src/HOL/Auth/All_Symmetric.thy
author wenzelm
Mon Jan 11 21:21:02 2016 +0100 (2016-01-11)
changeset 62145 5b946c81dfbf
parent 61830 4f5ab843cf5b
permissions -rw-r--r--
eliminated old defs;
     1 theory All_Symmetric
     2 imports Message
     3 begin
     4 
     5 text \<open>All keys are symmetric\<close>
     6 
     7 overloading all_symmetric \<equiv> all_symmetric
     8 begin
     9   definition "all_symmetric \<equiv> True"
    10 end
    11 
    12 lemma isSym_keys: "K \<in> symKeys"
    13   by (simp add: symKeys_def all_symmetric_def invKey_symmetric) 
    14 
    15 end