parent is Main
authorpaulson
Fri, 16 Oct 1998 12:20:41 +0200
changeset 5652 fe5f5510aef4
parent 5651 ca45d6126c8a
child 5653 204083e3f368
parent is Main
src/HOL/Auth/Message.thy
--- 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