changeset 5183 | 89f162de39cf |
parent 5102 | 8c782c25a11e |
child 5234 | 701fa0ed77b7 |
--- a/src/HOL/Auth/Message.thy Fri Jul 24 13:02:01 1998 +0200 +++ b/src/HOL/Auth/Message.thy Fri Jul 24 13:03:20 1998 +0200 @@ -7,7 +7,7 @@ Inductive relations "parts", "analz" and "synth" *) -Message = Arith + Inductive + +Message = Datatype + (*Is there a difference between a nonce and arbitrary numerical data? Do we need a type of nonces?*)