src/HOL/Auth/All_Symmetric.thy
author wenzelm
Mon Aug 31 21:28:08 2015 +0200 (2015-08-31)
changeset 61070 b72a990adfe2
parent 32631 2489e3c3562b
child 61830 4f5ab843cf5b
permissions -rw-r--r--
prefer symbols;
     1 theory All_Symmetric
     2 imports Message
     3 begin
     4 
     5 text {* All keys are symmetric *}
     6 
     7 defs all_symmetric_def: "all_symmetric \<equiv> True"
     8 
     9 lemma isSym_keys: "K \<in> symKeys"
    10   by (simp add: symKeys_def all_symmetric_def invKey_symmetric) 
    11 
    12 end