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