diff -r 37a6e2f55230 -r 44ff2275d44f IOA/example/Action.thy --- a/IOA/example/Action.thy Wed Nov 09 19:50:36 1994 +0100 +++ b/IOA/example/Action.thy Wed Nov 09 19:51:09 1994 +0100 @@ -1,3 +1,11 @@ +(* Title: HOL/IOA/example/Action.thy + ID: $Id$ + Author: Tobias Nipkow & Konrad Slind + Copyright 1994 TU Muenchen + +The set of all actions of the system +*) + Action = Packet + datatype 'm action = S_msg ('m) | R_msg ('m) | S_pkt ('m packet) | R_pkt ('m packet)