src/HOL/HOLCF/IOA/ABP/Abschannel.thy
changeset 66453 cc19f7ca2ed6
parent 62009 ecb5212d5885
equal deleted inserted replaced
66452:450cefec7c11 66453:cc19f7ca2ed6
     3 *)
     3 *)
     4 
     4 
     5 section \<open>The transmission channel\<close>
     5 section \<open>The transmission channel\<close>
     6 
     6 
     7 theory Abschannel
     7 theory Abschannel
     8 imports "../IOA" Action Lemmas
     8 imports IOA.IOA Action Lemmas
     9 begin
     9 begin
    10 
    10 
    11 datatype 'a abs_action = S 'a | R 'a
    11 datatype 'a abs_action = S 'a | R 'a
    12 
    12 
    13 
    13