| changeset 16417 | 9bc16273c2d4 |
| parent 15616 | cdf6eeb4ac27 |
| child 17990 | 86d462f305e0 |
--- a/src/HOL/Auth/Public.thy Fri Jun 17 11:35:35 2005 +0200 +++ b/src/HOL/Auth/Public.thy Fri Jun 17 16:12:49 2005 +0200 @@ -8,7 +8,7 @@ Private and public keys; initial states of agents *) -theory Public = Event: +theory Public imports Event begin lemma invKey_K: "K \<in> symKeys ==> invKey K = K" by (simp add: symKeys_def)