notations that resemble the ones used in the original paper. We believe
this a important part of every formalization, not only for the estetic
point of view, but also from the practical point of view. Being
-consistent allows to follow the paper in a pedantic way.
+consistent allows to follow the paper in a pedantic way, and hopefully
+to make the formalization (at least the definitions and proved
+statements) readable to the author of the paper.
Orientering
-----------
TODO
-buttons, PG-interaction-model, sequent window, script window
+buttons, PG-interaction-model, sequent window, script window, ncheck
The library, inclusion of `sets/sets.ma`, notation defined: Ω^A.
Symbols (see menu: View ▹ TeX/UTF-8 Table):