src/HOL/HOLCF/IOA/ABP/Action.thy
author wenzelm
Wed, 23 Jul 2025 14:53:21 +0200
changeset 82898 89da4dcd1fa8
parent 62002 f1599e98c4d0
permissions -rw-r--r--
clarified colors, following d6a14ed060fb;
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
42151
4da4fc77664b tuned headers;
wenzelm
parents: 40945
diff changeset
     1
(*  Title:      HOL/HOLCF/IOA/ABP/Action.thy
40945
b8703f63bfb2 recoded latin1 as utf8;
wenzelm
parents: 40774
diff changeset
     2
    Author:     Olaf Müller
3072
a31419014be5 Old ABP files now running under the IOA meta theory based on HOLCF;
mueller
parents:
diff changeset
     3
*)
a31419014be5 Old ABP files now running under the IOA meta theory based on HOLCF;
mueller
parents:
diff changeset
     4
62002
f1599e98c4d0 isabelle update_cartouches -c -t;
wenzelm
parents: 58880
diff changeset
     5
section \<open>The set of all actions of the system\<close>
17244
0b2ff9541727 converted to Isar theory format;
wenzelm
parents: 14981
diff changeset
     6
0b2ff9541727 converted to Isar theory format;
wenzelm
parents: 14981
diff changeset
     7
theory Action
0b2ff9541727 converted to Isar theory format;
wenzelm
parents: 14981
diff changeset
     8
imports Packet
0b2ff9541727 converted to Isar theory format;
wenzelm
parents: 14981
diff changeset
     9
begin
0b2ff9541727 converted to Isar theory format;
wenzelm
parents: 14981
diff changeset
    10
58310
91ea607a34d8 updated news
blanchet
parents: 58249
diff changeset
    11
datatype 'm action =
17244
0b2ff9541727 converted to Isar theory format;
wenzelm
parents: 14981
diff changeset
    12
    Next | S_msg 'm | R_msg 'm
0b2ff9541727 converted to Isar theory format;
wenzelm
parents: 14981
diff changeset
    13
  | S_pkt "'m packet" | R_pkt "'m packet"
0b2ff9541727 converted to Isar theory format;
wenzelm
parents: 14981
diff changeset
    14
  | S_ack bool | R_ack bool
0b2ff9541727 converted to Isar theory format;
wenzelm
parents: 14981
diff changeset
    15
3072
a31419014be5 Old ABP files now running under the IOA meta theory based on HOLCF;
mueller
parents:
diff changeset
    16
end