author | paulson |
Fri, 16 Oct 1998 12:20:41 +0200 | |
changeset 5652 | fe5f5510aef4 |
parent 5651 | ca45d6126c8a |
child 5653 | 204083e3f368 |
--- a/src/HOL/Auth/Message.thy Fri Oct 16 08:48:05 1998 +0200 +++ b/src/HOL/Auth/Message.thy Fri Oct 16 12:20:41 1998 +0200 @@ -7,10 +7,7 @@ Inductive relations "parts", "analz" and "synth" *) -Message = Datatype + - -(*Is there a difference between a nonce and arbitrary numerical data? - Do we need a type of nonces?*) +Message = Main + types key = nat