typo
authorkuncar
Wed, 08 Jan 2014 17:00:03 +0100
changeset 562899e632948ed56
parent 56288 1c000fa0fdf5
child 56291 26166d7f6a15
typo
src/HOL/Tools/Lifting/lifting_def.ML
     1.1 --- a/src/HOL/Tools/Lifting/lifting_def.ML	Wed Jan 08 16:59:57 2014 +0100
     1.2 +++ b/src/HOL/Tools/Lifting/lifting_def.ML	Wed Jan 08 17:00:03 2014 +0100
     1.3 @@ -55,7 +55,7 @@
     1.4    transfer_rule - of the form T t f
     1.5    parametric_transfer_rule - of the form par_R t' t
     1.6    
     1.7 -  Result: par_T t' f, after substituing op= for relations in par_T that relate
     1.8 +  Result: par_T t' f, after substituing op= for relations in par_R that relate
     1.9      a type constructor to the same type constructor, it is a merge of (par_R' OO T) t' f
    1.10      using Lifting_Term.merge_transfer_relations
    1.11  *)