src/HOL/Auth/All_Symmetric.thy
author wenzelm
Tue Sep 26 20:54:40 2017 +0200 (23 months ago)
changeset 66695 91500c024c7f
parent 62145 5b946c81dfbf
permissions -rw-r--r--
tuned;
haftmann@32631
     1
theory All_Symmetric
haftmann@32631
     2
imports Message
haftmann@32631
     3
begin
paulson@1944
     4
wenzelm@61830
     5
text \<open>All keys are symmetric\<close>
paulson@1944
     6
wenzelm@62145
     7
overloading all_symmetric \<equiv> all_symmetric
wenzelm@62145
     8
begin
wenzelm@62145
     9
  definition "all_symmetric \<equiv> True"
wenzelm@62145
    10
end
paulson@14145
    11
haftmann@32631
    12
lemma isSym_keys: "K \<in> symKeys"
haftmann@32631
    13
  by (simp add: symKeys_def all_symmetric_def invKey_symmetric) 
paulson@18886
    14
haftmann@32631
    15
end