src/HOLCF/IOA/meta_theory/Traces.ML
changeset 4536 74f7c556fd90
parent 4477 b3e5857d8d99
child 4559 8e604d885b54
equal deleted inserted replaced
4535:f24cebc299e4 4536:74f7c556fd90
     5 
     5 
     6 Theorems about Executions and Traces of I/O automata in HOLCF.
     6 Theorems about Executions and Traces of I/O automata in HOLCF.
     7 *)   
     7 *)   
     8 
     8 
     9 Delsimps (ex_simps @ all_simps);
     9 Delsimps (ex_simps @ all_simps);
       
    10 Delsimps [split_paired_Ex];
    10 
    11 
    11 val exec_rws = [executions_def,is_exec_frag_def];
    12 val exec_rws = [executions_def,is_exec_frag_def];
    12 
    13 
    13 
    14 
    14 
    15