src/HOLCF/IOA/meta_theory/Seq.thy
changeset 10835 f4745d77e620
parent 5976 44290b71a85f
child 12218 6597093b77e7
     1.1 --- a/src/HOLCF/IOA/meta_theory/Seq.thy	Tue Jan 09 15:32:27 2001 +0100
     1.2 +++ b/src/HOLCF/IOA/meta_theory/Seq.thy	Tue Jan 09 15:36:30 2001 +0100
     1.3 @@ -36,7 +36,7 @@
     1.4     "Finite"     :: "'a seq => bool"
     1.5  
     1.6  translations
     1.7 -   "xs @@ ys" == "sconc`xs`ys"
     1.8 +   "xs @@ ys" == "sconc$xs$ys"
     1.9     "Finite x" == "x:sfinite"
    1.10     "~(Finite x)" =="x~:sfinite"
    1.11  
    1.12 @@ -47,63 +47,63 @@
    1.13  (* f not possible at lhs, as "pattern matching" only for % x arguments,
    1.14     f cannot be written at rhs in front, as fix_eq3 does not apply later *)
    1.15  smap_def
    1.16 -  "smap == (fix`(LAM h f tr. case tr of 
    1.17 +  "smap == (fix$(LAM h f tr. case tr of 
    1.18        nil   => nil
    1.19 -    | x##xs => f`x ## h`f`xs))"
    1.20 +    | x##xs => f$x ## h$f$xs))"
    1.21  
    1.22  sfilter_def       
    1.23 -  "sfilter == (fix`(LAM h P t. case t of 
    1.24 +  "sfilter == (fix$(LAM h P t. case t of 
    1.25  	   nil => nil
    1.26 -	 | x##xs => If P`x                                 
    1.27 -                    then x##(h`P`xs)
    1.28 -                    else     h`P`xs
    1.29 +	 | x##xs => If P$x                                 
    1.30 +                    then x##(h$P$xs)
    1.31 +                    else     h$P$xs
    1.32                      fi))" 
    1.33  sforall_def
    1.34 -  "sforall P t == (sforall2`P`t ~=FF)" 
    1.35 +  "sforall P t == (sforall2$P$t ~=FF)" 
    1.36  
    1.37  
    1.38  sforall2_def
    1.39 -  "sforall2 == (fix`(LAM h P t. case t of 
    1.40 +  "sforall2 == (fix$(LAM h P t. case t of 
    1.41  	   nil => TT
    1.42 -	 | x##xs => P`x andalso h`P`xs))"
    1.43 +	 | x##xs => P$x andalso h$P$xs))"
    1.44    
    1.45  sconc_def
    1.46 -  "sconc == (fix`(LAM h t1 t2. case t1 of 
    1.47 +  "sconc == (fix$(LAM h t1 t2. case t1 of 
    1.48                 nil       => t2
    1.49 -             | x##xs => x##(h`xs`t2)))"
    1.50 +             | x##xs => x##(h$xs$t2)))"
    1.51  
    1.52  slast_def
    1.53 -  "slast == (fix`(LAM h t. case t of 
    1.54 +  "slast == (fix$(LAM h t. case t of 
    1.55  	   nil => UU
    1.56 -	 | x##xs => (If is_nil`xs                              
    1.57 +	 | x##xs => (If is_nil$xs                              
    1.58                            then x
    1.59 -                         else h`xs fi)))"
    1.60 +                         else h$xs fi)))"
    1.61  
    1.62  stakewhile_def      
    1.63 -  "stakewhile == (fix`(LAM h P t. case t of 
    1.64 +  "stakewhile == (fix$(LAM h P t. case t of 
    1.65  	   nil => nil
    1.66 -	 | x##xs => If P`x                                 
    1.67 -                    then x##(h`P`xs)
    1.68 +	 | x##xs => If P$x                                 
    1.69 +                    then x##(h$P$xs)
    1.70                      else nil
    1.71                      fi))" 
    1.72  sdropwhile_def
    1.73 -  "sdropwhile == (fix`(LAM h P t. case t of 
    1.74 +  "sdropwhile == (fix$(LAM h P t. case t of 
    1.75  	   nil => nil
    1.76 -	 | x##xs => If P`x                                 
    1.77 -                    then h`P`xs
    1.78 +	 | x##xs => If P$x                                 
    1.79 +                    then h$P$xs
    1.80                      else t
    1.81                      fi))" 
    1.82  sflat_def
    1.83 -  "sflat == (fix`(LAM h t. case t of 
    1.84 +  "sflat == (fix$(LAM h t. case t of 
    1.85  	   nil => nil
    1.86 -	 | x##xs => x @@ (h`xs)))"
    1.87 +	 | x##xs => x @@ (h$xs)))"
    1.88  
    1.89  szip_def
    1.90 -  "szip == (fix`(LAM h t1 t2. case t1 of 
    1.91 +  "szip == (fix$(LAM h t1 t2. case t1 of 
    1.92                 nil   => nil
    1.93               | x##xs => (case t2 of 
    1.94                            nil => UU 
    1.95 -                        | y##ys => <x,y>##(h`xs`ys))))"
    1.96 +                        | y##ys => <x,y>##(h$xs$ys))))"
    1.97  
    1.98  Partial_def
    1.99    "Partial x  == (seq_finite x) & ~(Finite x)"