(* Title: HOL/IOA/NTP/Packet.thy ID: $Id$ Author: Tobias Nipkow & Konrad Slind Copyright 1994 TU Muenchen Packets *) Packet = Arith + Multiset + types 'msg packet = "bool * 'msg" consts hdr :: 'msg packet => bool msg :: 'msg packet => 'msg defs hdr_def "hdr == fst" msg_def "msg == snd" end