src/HOL/Auth/All_Symmetric.thy
author blanchet
Thu, 18 Feb 2010 18:48:07 +0100
changeset 35220 2bcdae5f4fdb
parent 32631 2489e3c3562b
child 61830 4f5ab843cf5b
permissions -rw-r--r--
added support for nonstandard "nat"s to Nitpick and fixed bugs in binary "nat"s and "int"s

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