equal
deleted
inserted
replaced
|
1 theory All_Symmetric |
|
2 imports Message |
|
3 begin |
|
4 |
|
5 text {* All keys are symmetric *} |
|
6 |
|
7 defs all_symmetric_def: "all_symmetric \<equiv> True" |
|
8 |
|
9 lemma isSym_keys: "K \<in> symKeys" |
|
10 by (simp add: symKeys_def all_symmetric_def invKey_symmetric) |
|
11 |
|
12 end |