Up to index of Isabelle/HOLCF/IOA/NTP
theory Packet(* 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