src/HOL/HOLCF/IOA/ABP/Action.thy
author blanchet
Tue, 09 Sep 2014 20:51:36 +0200
changeset 58249 180f1b3508ed
parent 42151 4da4fc77664b
child 58310 91ea607a34d8
permissions -rw-r--r--
use 'datatype_new' (soon to be renamed 'datatype') in Isabelle's libraries
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
17244
0b2ff9541727 converted to Isar theory format;
wenzelm
parents: 14981
diff changeset
     5
header {* The set of all actions of the system *}
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
58249
180f1b3508ed use 'datatype_new' (soon to be renamed 'datatype') in Isabelle's libraries
blanchet
parents: 42151
diff changeset
    11
datatype_new '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