parent is Main
authorpaulson
Fri Oct 16 12:20:41 1998 +0200 (1998-10-16)
changeset 5652fe5f5510aef4
parent 5651 ca45d6126c8a
child 5653 204083e3f368
parent is Main
src/HOL/Auth/Message.thy
     1.1 --- a/src/HOL/Auth/Message.thy	Fri Oct 16 08:48:05 1998 +0200
     1.2 +++ b/src/HOL/Auth/Message.thy	Fri Oct 16 12:20:41 1998 +0200
     1.3 @@ -7,10 +7,7 @@
     1.4  Inductive relations "parts", "analz" and "synth"
     1.5  *)
     1.6  
     1.7 -Message = Datatype +
     1.8 -
     1.9 -(*Is there a difference between a nonce and arbitrary numerical data?
    1.10 -  Do we need a type of nonces?*)
    1.11 +Message = Main +
    1.12  
    1.13  types 
    1.14    key = nat