src/HOLCF/IOA/NTP/Packet.thy

- Installed specific code generator for equality enforcing that
arguments do not have function types, which would result in
an error message during compilation.

- Added test case generators for basic types.

(*  Title:      HOL/IOA/NTP/Packet.thy
    ID:         $Id$
    Author:     Tobias Nipkow & Konrad Slind
    License:    GPL (GNU GENERAL PUBLIC LICENSE)

Packets.
*)

Packet = Multiset +  

types

   'msg packet = "bool * 'msg"

constdefs

  hdr  :: 'msg packet => bool
  "hdr == fst"

  msg :: 'msg packet => 'msg
  "msg == snd"

end