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