Hi.
I seem to recall reading that in TLA+ a tagged formula means the formula with all variables tagged. TLC does not seem to be of the same opinion; as a result I sometimes find myself writing the same formula twice -- for the tagged and untagged variables. Did I misunderstand or is this a TLA+ feature unsupported by TLC?
Ron