| author | huffman |
| Sat, 27 Nov 2010 16:08:10 -0800 | |
| changeset 41022 | 0437dbc127b3 |
| parent 35174 | src/HOLCF/IOA/NTP/Packet.thy@e15040ae75d7 |
| child 41724 | 0fa9629aa399 |
| permissions | -rw-r--r-- |
1 (* Title: HOL/IOA/NTP/Packet.thy
2 Author: Tobias Nipkow & Konrad Slind
3 *)
5 theory Packet
6 imports Multiset
7 begin
9 types
10 'msg packet = "bool * 'msg"
12 definition
13 hdr :: "'msg packet => bool" where
14 "hdr == fst"
16 definition
17 msg :: "'msg packet => 'msg" where
18 "msg == snd"
21 text {* Instantiation of a tautology? *}
22 lemma eq_packet_imp_eq_hdr: "!x. x = packet --> hdr(x) = hdr(packet)"
23 by simp
25 declare hdr_def [simp] msg_def [simp]
27 end