Appendix A

予約語一覧表


A.1 Mizar チェッカー(アコモデータも含む)


  aggregate  and   antonym

  as  assume   attr

be begin being

by canceled case

cases cluster coherence

compatibility consider consistency

contradiction correctness def

deffunc define definition

defpred end enviorn

ex exactly existence

for from func

given hence hereby

holds if iff

implies is it

let means mode

non not now

of or otherwise

over per pred

prefix proof provided

qua reconsider redefine

reserve schme selector

set st struct

take that the

then thesis theorem

thus uniqueness where


A.2 アコモデータのみ


vocabulary constructors signature

definitions clusters theorems

schemes notations