author | paulson |
Fri, 05 Oct 2007 09:59:03 +0200 | |
changeset 24854 | 0ebcd575d3c6 |
parent 19738 | 1ac610922636 |
child 25131 | 2c8caac48ade |
permissions | -rw-r--r-- |
3072
a31419014be5
Old ABP files now running under the IOA meta theory based on HOLCF;
mueller
parents:
diff
changeset
|
1 |
(* Title: HOLCF/IOA/ABP/Packet.thy |
a31419014be5
Old ABP files now running under the IOA meta theory based on HOLCF;
mueller
parents:
diff
changeset
|
2 |
ID: $Id$ |
12218 | 3 |
Author: Olaf Müller |
3072
a31419014be5
Old ABP files now running under the IOA meta theory based on HOLCF;
mueller
parents:
diff
changeset
|
4 |
*) |
a31419014be5
Old ABP files now running under the IOA meta theory based on HOLCF;
mueller
parents:
diff
changeset
|
5 |
|
17244 | 6 |
header {* Packets *} |
7 |
||
8 |
theory Packet |
|
9 |
imports Main |
|
10 |
begin |
|
3072
a31419014be5
Old ABP files now running under the IOA meta theory based on HOLCF;
mueller
parents:
diff
changeset
|
11 |
|
a31419014be5
Old ABP files now running under the IOA meta theory based on HOLCF;
mueller
parents:
diff
changeset
|
12 |
types |
17244 | 13 |
'msg packet = "bool * 'msg" |
3072
a31419014be5
Old ABP files now running under the IOA meta theory based on HOLCF;
mueller
parents:
diff
changeset
|
14 |
|
a31419014be5
Old ABP files now running under the IOA meta theory based on HOLCF;
mueller
parents:
diff
changeset
|
15 |
constdefs |
17244 | 16 |
hdr :: "'msg packet => bool" |
3072
a31419014be5
Old ABP files now running under the IOA meta theory based on HOLCF;
mueller
parents:
diff
changeset
|
17 |
"hdr == fst" |
a31419014be5
Old ABP files now running under the IOA meta theory based on HOLCF;
mueller
parents:
diff
changeset
|
18 |
|
17244 | 19 |
msg :: "'msg packet => 'msg" |
3072
a31419014be5
Old ABP files now running under the IOA meta theory based on HOLCF;
mueller
parents:
diff
changeset
|
20 |
"msg == snd" |
a31419014be5
Old ABP files now running under the IOA meta theory based on HOLCF;
mueller
parents:
diff
changeset
|
21 |
|
a31419014be5
Old ABP files now running under the IOA meta theory based on HOLCF;
mueller
parents:
diff
changeset
|
22 |
end |