src/HOLCF/IOA/meta_theory/Traces.thy
changeset 12338 de0f4a63baa5
parent 12218 6597093b77e7
child 14981 e73f8140af78
equal deleted inserted replaced
12337:7c6a970f0808 12338:de0f4a63baa5
     7 *)   
     7 *)   
     8 
     8 
     9 		       
     9 		       
    10 Traces = Sequence + Automata +
    10 Traces = Sequence + Automata +
    11 
    11 
    12 default term
    12 default type
    13  
    13  
    14 types  
    14 types  
    15    ('a,'s)pairs            =    "('a * 's) Seq"
    15    ('a,'s)pairs            =    "('a * 's) Seq"
    16    ('a,'s)execution        =    "'s * ('a,'s)pairs"
    16    ('a,'s)execution        =    "'s * ('a,'s)pairs"
    17    'a trace                =    "'a Seq"
    17    'a trace                =    "'a Seq"