[tlaplus] About WF and SF operators' semantics

Folks,

I realized that Hillel Wayne's writing about WF and SF is really awesome for me to understand clearly(hope so) the two concepts.
( https://www.hillelwayne.com/post/fairness/ )
----------------------------------------------------------------------
WF_v(A) == <>[](ENABLED <<A>>_v) => []<><<A>>_v

//Weak Fairness: If eventually ALWAYS/KEEP enabled, then will be ALWAYS be EVENTUALLY（Or say, infinitely many) executed.

SF_v(A) == []<>ENABLED <<A>>_v => []<><<A>>_v

//Strong Fairness: If NOT NEVER disabled(means could happen sometimes and many times), then will be ALWAYS be EVENTUALLY（Or say, infinitely many) executed.

------------------------------------------------------------

Wayne's explanation is pretty consistent with Lamport's old-tla-src paper(section 3.2) written in 1990.

But, if we read Lamport's 1994 ACM paper, the description was changed by using a more abstracted way as:

//Page 13, ACM Trans on Programming and Systems.

weak fairness: ([]<> executed) ∨ ([]<> impossible)
strong fairness: ([]<> executed) ∨ (<>[] impossible)

WFf(A) == ([]<>⟨A⟩f) ∨ ([]<> ¬ Enabled ⟨A⟩f)
SFf(A) == ([]<>⟨A⟩f) ∨ (<>[]¬Enabled ⟨A⟩f)

------------------------------------

While I believe Wayne's logic formula for WF and SF is equal to that above in Lamports' 1994 paper, I am wondering why Dr. Lamport changed this part‘上writing from his 1990's paper.

Or should we read Lamport's 1990's TLA paper? What's the difference between the 1990's and the 1994's?

Thanks,

Huailin