milestone update in ground

[helm.git] / matita / matita / contribs / lambdadelta / ground / counters / rtc_ist.ma

diff --git a/matita/matita/contribs/lambdadelta/ground/counters/rtc_ist.ma b/matita/matita/contribs/lambdadelta/ground/counters/rtc_ist.ma
index 38c430ae87a3d3bed032024dfd9448a0a5c610e4..57ba73e327d5bcf0e32cfe75b4c1a72605de3064 100644 (file)
--- 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 ******************************************************)