1theory All_Symmetric 2imports Message 3begin 4 5text \<open>All keys are symmetric\<close> 6 7overloading all_symmetric \<equiv> all_symmetric 8begin 9 definition "all_symmetric \<equiv> True" 10end 11 12lemma isSym_keys: "K \<in> symKeys" 13 by (simp add: symKeys_def all_symmetric_def invKey_symmetric) 14 15end 16