src/HOLCF/IOA/NTP/Packet.ML
author kleing
Mon Jun 21 10:25:57 2004 +0200 (2004-06-21)
changeset 14981 e73f8140af78
parent 12218 6597093b77e7
child 17244 0b2ff9541727
permissions -rw-r--r--
Merged in license change from Isabelle2004
mueller@3073
     1
(*  Title:      HOL/IOA/NTP/Packet.ML
mueller@3073
     2
    ID:         $Id$
mueller@3073
     3
    Author:     Tobias Nipkow & Konrad Slind
mueller@3073
     4
wenzelm@12218
     5
Packets.
mueller@3073
     6
*)
mueller@3073
     7
mueller@3073
     8
(* Instantiation of a tautology? *)
wenzelm@5068
     9
Goal "!x. x = packet --> hdr(x) = hdr(packet)";
wenzelm@4098
    10
 by (simp_tac (simpset() addsimps [Packet.hdr_def]) 1);
mueller@3073
    11
qed "eq_packet_imp_eq_hdr"; 
mueller@3073
    12
mueller@3073
    13
Addsimps [Packet.hdr_def,Packet.msg_def];