1(*  Title:      HOL/HOLCF/IOA/ABP/Packet.thy
2    Author:     Olaf M��ller
3*)
4
5section \<open>Packets\<close>
6
7theory Packet
8imports Main
9begin
10
11type_synonym
12  'msg packet = "bool * 'msg"
13
14definition
15  hdr :: "'msg packet => bool" where
16  "hdr = fst"
17
18definition
19  msg :: "'msg packet => 'msg" where
20  "msg = snd"
21
22end
23