changeset 45827 | 66c68453455c |
parent 39758 | b8a53e3a0ee2 |
child 51717 | 9e7d1c139569 |
--- a/src/HOL/SET_Protocol/Public_SET.thy Tue Dec 13 14:04:20 2011 +0100 +++ b/src/HOL/SET_Protocol/Public_SET.thy Tue Dec 13 15:18:52 2011 +0100 @@ -46,7 +46,7 @@ done (*>*) -axioms +axiomatization where (*No private key equals any public key (essential to ensure that private keys are private!) *) privateKey_neq_publicKey [iff]: