changeset 5652 | fe5f5510aef4 |
parent 5234 | 701fa0ed77b7 |
child 6807 | 6737af18317e |
--- 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