| changeset 1266 | 3ae9fe3c0f68 |
| parent 1051 | 4fcd0638e61d |
| child 1328 | 9a449a91425d |
| 1265:6ef9a9893fd6 | 1266:3ae9fe3c0f68 |
|---|---|
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 Packet.thy "!x. x = packet --> hdr(x) = hdr(packet)"; |
12 by (simp_tac (HOL_ss 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"; |