equal
deleted
inserted
replaced
12 declare [[metis_new_skolemizer]] |
12 declare [[metis_new_skolemizer]] |
13 |
13 |
14 lemma strange_Un_eq [simp]: "A \<union> (B \<union> A) = B \<union> A" |
14 lemma strange_Un_eq [simp]: "A \<union> (B \<union> A) = B \<union> A" |
15 by (metis Un_commute Un_left_absorb) |
15 by (metis Un_commute Un_left_absorb) |
16 |
16 |
17 types |
17 type_synonym key = nat |
18 key = nat |
|
19 |
18 |
20 consts |
19 consts |
21 all_symmetric :: bool --{*true if all keys are symmetric*} |
20 all_symmetric :: bool --{*true if all keys are symmetric*} |
22 invKey :: "key=>key" --{*inverse of a symmetric key*} |
21 invKey :: "key=>key" --{*inverse of a symmetric key*} |
23 |
22 |