changeset 25131 | 2c8caac48ade |
parent 19739 | c58ef2aa5430 |
child 35174 | e15040ae75d7 |
--- a/src/HOLCF/IOA/NTP/Packet.thy Sun Oct 21 14:21:45 2007 +0200 +++ b/src/HOLCF/IOA/NTP/Packet.thy Sun Oct 21 14:21:48 2007 +0200 @@ -10,12 +10,12 @@ types 'msg packet = "bool * 'msg" -constdefs - - hdr :: "'msg packet => bool" +definition + hdr :: "'msg packet => bool" where "hdr == fst" - msg :: "'msg packet => 'msg" +definition + msg :: "'msg packet => 'msg" where "msg == snd"