IOA/example/Packet.thy

added IOA to isabelle/HOL

Packet = Arith +

types

   'msg packet = "bool * 'msg"

consts

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

rules

  hdr_def "hdr == fst"

  msg_def "msg == snd"

end