src/HOL/Auth/All_Symmetric.thy
author wenzelm
Thu Dec 10 21:39:33 2015 +0100 (2015-12-10)
changeset 61830 4f5ab843cf5b
parent 32631 2489e3c3562b
child 62145 5b946c81dfbf
permissions -rw-r--r--
isabelle update_cartouches -c -t;
     1 theory All_Symmetric
     2 imports Message
     3 begin
     4 
     5 text \<open>All keys are symmetric\<close>
     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