IOA/example/Packet.thy
author clasohm
Wed, 02 Nov 1994 11:50:09 +0100
changeset 156 fd1be45b64bf
child 168 44ff2275d44f
permissions -rw-r--r--
added IOA to isabelle/HOL
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
156
fd1be45b64bf added IOA to isabelle/HOL
clasohm
parents:
diff changeset
     1
Packet = Arith +
fd1be45b64bf added IOA to isabelle/HOL
clasohm
parents:
diff changeset
     2
fd1be45b64bf added IOA to isabelle/HOL
clasohm
parents:
diff changeset
     3
types
fd1be45b64bf added IOA to isabelle/HOL
clasohm
parents:
diff changeset
     4
fd1be45b64bf added IOA to isabelle/HOL
clasohm
parents:
diff changeset
     5
   'msg packet = "bool * 'msg"
fd1be45b64bf added IOA to isabelle/HOL
clasohm
parents:
diff changeset
     6
fd1be45b64bf added IOA to isabelle/HOL
clasohm
parents:
diff changeset
     7
consts
fd1be45b64bf added IOA to isabelle/HOL
clasohm
parents:
diff changeset
     8
fd1be45b64bf added IOA to isabelle/HOL
clasohm
parents:
diff changeset
     9
  hdr  :: "'msg packet => bool"
fd1be45b64bf added IOA to isabelle/HOL
clasohm
parents:
diff changeset
    10
  msg :: "'msg packet => 'msg"
fd1be45b64bf added IOA to isabelle/HOL
clasohm
parents:
diff changeset
    11
fd1be45b64bf added IOA to isabelle/HOL
clasohm
parents:
diff changeset
    12
rules
fd1be45b64bf added IOA to isabelle/HOL
clasohm
parents:
diff changeset
    13
fd1be45b64bf added IOA to isabelle/HOL
clasohm
parents:
diff changeset
    14
  hdr_def "hdr == fst"
fd1be45b64bf added IOA to isabelle/HOL
clasohm
parents:
diff changeset
    15
fd1be45b64bf added IOA to isabelle/HOL
clasohm
parents:
diff changeset
    16
  msg_def "msg == snd"
fd1be45b64bf added IOA to isabelle/HOL
clasohm
parents:
diff changeset
    17
fd1be45b64bf added IOA to isabelle/HOL
clasohm
parents:
diff changeset
    18
end