-
Robbert Krebbers authored
After discussing this with Ralf, again, it turned out that using a bar instead of a turnstyle would be better. When formalizing type systems, one often wants to use a turnstyle in other notations (the typing judgment), so having the turnstyle in the proofmode notation is confusing.
293fb6c7