src/HOL/IOA/ABP/Abschannel_finite.thy
changeset 1376 92f83b9d17e1
parent 1151 c820b3cc3df0
child 1476 608483c2122a
     1.1 --- a/src/HOL/IOA/ABP/Abschannel_finite.thy	Thu Nov 30 12:58:44 1995 +0100
     1.2 +++ b/src/HOL/IOA/ABP/Abschannel_finite.thy	Fri Dec 01 12:03:13 1995 +0100
     1.3 @@ -10,22 +10,22 @@
     1.4   
     1.5  consts
     1.6   
     1.7 -ch_fin_asig  :: "'a act signature"
     1.8 +ch_fin_asig  :: 'a act signature
     1.9  
    1.10 -ch_fin_trans :: "('a act, 'a list)transition set"
    1.11 +ch_fin_trans :: ('a act, 'a list)transition set
    1.12  
    1.13 -ch_fin_ioa   :: "('a act, 'a list)ioa"
    1.14 +ch_fin_ioa   :: ('a act, 'a list)ioa
    1.15  
    1.16  srch_fin_asig, 
    1.17 -rsch_fin_asig  :: "'m action signature"
    1.18 +rsch_fin_asig  :: 'm action signature
    1.19  
    1.20 -srch_fin_trans :: "('m action, 'm packet list)transition set"
    1.21 -rsch_fin_trans :: "('m action, bool list)transition set"
    1.22 +srch_fin_trans :: ('m action, 'm packet list)transition set
    1.23 +rsch_fin_trans :: ('m action, bool list)transition set
    1.24  
    1.25 -srch_fin_ioa   :: "('m action, 'm packet list)ioa"
    1.26 -rsch_fin_ioa   :: "('m action, bool list)ioa"   
    1.27 +srch_fin_ioa   :: ('m action, 'm packet list)ioa
    1.28 +rsch_fin_ioa   :: ('m action, bool list)ioa   
    1.29  
    1.30 -reverse        :: "'a list => 'a list"
    1.31 +reverse        :: 'a list => 'a list
    1.32  
    1.33  primrec
    1.34    reverse List.list