src/HOL/Auth/All_Symmetric.thy
author blanchet
Thu, 24 Jul 2014 00:24:00 +0200
changeset 57631 959caab43a3d
parent 32631 2489e3c3562b
child 61830 4f5ab843cf5b
permissions -rw-r--r--
use the noted theorem whenever possible, also in 'BNF_Def'

theory All_Symmetric
imports Message
begin

text {* All keys are symmetric *}

defs all_symmetric_def: "all_symmetric \<equiv> True"

lemma isSym_keys: "K \<in> symKeys"
  by (simp add: symKeys_def all_symmetric_def invKey_symmetric) 

end