Appendix A

List of Reserved Words


A.1 Mizar Checker (including the accomodation data)


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 Only the Accomodation Data


vocabulary constructors signature

definitions clusters theorems

schemes notations