IOA/example/Packet.thy
changeset 156 fd1be45b64bf
child 168 44ff2275d44f
equal deleted inserted replaced
155:722bf1319be5 156:fd1be45b64bf
       
     1 Packet = Arith +
       
     2 
       
     3 types
       
     4 
       
     5    'msg packet = "bool * 'msg"
       
     6 
       
     7 consts
       
     8 
       
     9   hdr  :: "'msg packet => bool"
       
    10   msg :: "'msg packet => 'msg"
       
    11 
       
    12 rules
       
    13 
       
    14   hdr_def "hdr == fst"
       
    15 
       
    16   msg_def "msg == snd"
       
    17 
       
    18 end