X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2Fmatita%2Fcontribs%2Flambdadelta%2Fground%2Fcounters%2Frtc_ist.ma;h=57ba73e327d5bcf0e32cfe75b4c1a72605de3064;hb=55c768d7e45babb300b5010463ba3196a68f1bbe;hp=38c430ae87a3d3bed032024dfd9448a0a5c610e4;hpb=15212e44902f25536f6e2de4bec4cedcd9a9804d;p=helm.git

diff --git a/matita/matita/contribs/lambdadelta/ground/counters/rtc_ist.ma b/matita/matita/contribs/lambdadelta/ground/counters/rtc_ist.ma
index 38c430ae8..57ba73e32 100644
--- a/matita/matita/contribs/lambdadelta/ground/counters/rtc_ist.ma
+++ b/matita/matita/contribs/lambdadelta/ground/counters/rtc_ist.ma
@@ -12,7 +12,7 @@
 (*                                                                        *)
 (**************************************************************************)
 
-include "ground/notation/relations/ist_2.ma".
+include "ground/notation/relations/predicate_t_2.ma".
 include "ground/counters/rtc.ma".
 
 (* T-TRANSITION COUNTERS ****************************************************)
@@ -21,8 +21,8 @@ definition rtc_ist: relation2 nat rtc ≝
            λts,c. 〈𝟎,𝟎,𝟎,ts〉 = c.
 
 interpretation
-  "t-transition counters (rtc)"
-  'IsT ts c = (rtc_ist ts c).
+  "construction (t-transition counters)"
+  'PredicateT ts c = (rtc_ist ts c).
 
 (* Basic constructions ******************************************************)