equal
deleted
inserted
replaced
6 Packets |
6 Packets |
7 *) |
7 *) |
8 |
8 |
9 |
9 |
10 (* Instantiation of a tautology? *) |
10 (* Instantiation of a tautology? *) |
11 goal Packet.thy "!x. x = packet --> hdr(x) = hdr(packet)"; |
11 Goal "!x. x = packet --> hdr(x) = hdr(packet)"; |
12 by (simp_tac (simpset() addsimps [Packet.hdr_def]) 1); |
12 by (simp_tac (simpset() addsimps [Packet.hdr_def]) 1); |
13 qed "eq_packet_imp_eq_hdr"; |
13 qed "eq_packet_imp_eq_hdr"; |
14 |
14 |
15 Addsimps [Packet.hdr_def,Packet.msg_def]; |
15 Addsimps [Packet.hdr_def,Packet.msg_def]; |