I presume that by "tagged" you mean primed. Yes, e' means e with all variables in it primed. Please tell us exactly what TLC is not interpreting as you expect it to.
Leslie
On Wednesday, January 6, 2016 at 9:39:20 AM UTC-8, Ron Pressler wrote:
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