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;
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