Version 1.2

Fixes a syntactically incorrect theorem definition involving TypeOK.

Version 1.1

Adding additional theorems to make clear what invariants are supposed to hold.

Version 1.0

Version 1.0 of a TLA+ specification of Peterson's algorithm.