equal
deleted
inserted
replaced
8 begin |
8 begin |
9 |
9 |
10 types |
10 types |
11 'msg packet = "bool * 'msg" |
11 'msg packet = "bool * 'msg" |
12 |
12 |
13 constdefs |
13 definition |
14 |
14 hdr :: "'msg packet => bool" where |
15 hdr :: "'msg packet => bool" |
|
16 "hdr == fst" |
15 "hdr == fst" |
17 |
16 |
18 msg :: "'msg packet => 'msg" |
17 definition |
|
18 msg :: "'msg packet => 'msg" where |
19 "msg == snd" |
19 "msg == snd" |
20 |
20 |
21 |
21 |
22 text {* Instantiation of a tautology? *} |
22 text {* Instantiation of a tautology? *} |
23 lemma eq_packet_imp_eq_hdr: "!x. x = packet --> hdr(x) = hdr(packet)" |
23 lemma eq_packet_imp_eq_hdr: "!x. x = packet --> hdr(x) = hdr(packet)" |