make WWW_Find work again, now that its ML modules reside within a theory context (cf. bf5b45870110) -- patch by Rafal Kolanski;
(* Title: HOL/HOLCF/IOA/ABP/Packet.thy
Author: Olaf Müller
*)
header {* Packets *}
theory Packet
imports Main
begin
type_synonym
'msg packet = "bool * 'msg"
definition
hdr :: "'msg packet => bool" where
"hdr = fst"
definition
msg :: "'msg packet => 'msg" where
"msg = snd"
end