# HG changeset patch
# User kuncar
# Date 1392303114 -3600
# Node ID e373c9f60db1055830befa3c138d4d1d67537f5f
# Parent  a422f93eae0d061e52663b03a6c52cf41de05d0d
more precise descripiton

diff -r a422f93eae0d -r e373c9f60db1 src/HOL/Tools/Lifting/lifting_term.ML
--- a/src/HOL/Tools/Lifting/lifting_term.ML	Thu Feb 13 14:32:05 2014 +0100
+++ b/src/HOL/Tools/Lifting/lifting_term.ML	Thu Feb 13 15:51:54 2014 +0100
@@ -460,11 +460,13 @@
 in
 
   (*
-    ctm - of the form (par_R OO T) t f, where par_R is a parametricity transfer relation for t
-      and T is a transfer relation between t and f.
+    ctm - of the form "[POS|NEG] (par_R OO T) t f) ?X", where par_R is a parametricity transfer 
+    relation for t and T is a transfer relation between t and f, which consists only from
+    parametrized transfer relations (i.e., pcr_?) and equalities op=. POS or NEG encodes
+    co-variance or contra-variance.
     
     The function merges par_R OO T using definitions of parametrized correspondence relations
-    (e.g., rel_T R OO cr_T == pcr_T R).
+    (e.g., (rel_S R) OO (pcr_T op=) --> pcr_T R using the definition pcr_T R = (rel_S R) OO cr_T).
   *)
 
   fun merge_transfer_relations ctxt ctm =