4.5.1 end についての注意

 end についての注意ですが,Mizarでは,proof-end,now-end などで end が出てきて,またこれらがネスティングをなしてきます.end がたくさんあると,どれがどの end かわからなくなってしまいます.ですから now を書いたら end は必要なので,now を書いたら end をすぐに書いてしまいます.あとは,この中にエディターでどんどん挿入していけばいいわけです.同様に,proof と書いたら,必ずend と書いてしまいます.end だけを書くということはないと決めておくと間違いはありません.