| changeset 35416 | d8d7d1b785af |
| parent 32960 | 69916a850301 |
| child 37936 | 1e4c5015a72e |
--- a/src/HOL/Auth/CertifiedEmail.thy Wed Feb 24 11:55:52 2010 +0100 +++ b/src/HOL/Auth/CertifiedEmail.thy Mon Mar 01 13:40:23 2010 +0100 @@ -25,8 +25,7 @@ BothAuth :: nat text{*We formalize a fixed way of computing responses. Could be better.*} -constdefs - "response" :: "agent => agent => nat => msg" +definition "response" :: "agent => agent => nat => msg" where "response S R q == Hash {|Agent S, Key (shrK R), Nonce q|}"