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