# Theory Packet

Up to index of Isabelle/HOLCF/IOA/NTP

theory Packet
imports Multiset
uses [Packet.ML]
begin

    (*  Title:      HOL/IOA/NTP/Packet.thy
        ID:         $Id: Packet.thy,v 1.5 2005/09/03 14:50:24 wenzelm Exp $
        Author:     Tobias Nipkow & Konrad Slind
    *)

    theory Packet
    imports Multiset
    begin

    types
      'msg packet = "bool * 'msg"

    constdefs

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

      msg :: "'msg packet => 'msg"
      "msg == snd"

    ML {* use_legacy_bindings (the_context ()) *}

    end

theorem eq_packet_imp_eq_hdr:

      ∀x. x = packet --> hdr x = hdr packet