milestone update in ground

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

diff --git a/matita/matita/contribs/lambdadelta/ground/counters/rtc_ism.ma b/matita/matita/contribs/lambdadelta/ground/counters/rtc_ism.ma
index 335bbbc905884dd23bce5a491bdd6c698f0a6d3e..3b8cbfe9c7c8485ca0ae179b29d6ee4f230c21a2 100644 (file)
--- a/matita/matita/contribs/lambdadelta/ground/counters/rtc_ism.ma
+++ b/matita/matita/contribs/lambdadelta/ground/counters/rtc_ism.ma
@@ -12,7 +12,7 @@
 (*                                                                        *)
 (**************************************************************************)
 
-include "ground/notation/relations/ism_2.ma".
+include "ground/notation/relations/predicate_m_2.ma".
 include "ground/counters/rtc.ma".
 
 (* T-BOUND RT-TRANSITION COUNTERS *******************************************)
@@ -21,8 +21,8 @@ definition rtc_ism: relation2 nat rtc ≝ λts,c.
            ∃∃ri,rs. 〈ri,rs,𝟎,ts〉 = c.
 
 interpretation
-  "t-bound rt-transition counters (rtc)"
-  'IsM ts c = (rtc_ism ts c).
+  "construction (t-bound rt-transition counters)"
+  'PredicateM ts c = (rtc_ism ts c).
 
 (* Basic constructions ******************************************************)