Size of Mizar/MML

Dear Mizar Community,

I am currently creating a comparison of large libraries of ITPs. I am 
only considering libraries with more than 1M (nonempty) LOC, of which I 
know (in alphabetical order): ACL2, HOL4, Isabelle, Lean, Metamath, 
Mizar, PVS, Rocq.
To that end, I want to approximate the number of definitions (incl. 
axioms / excl. abbreviations, instances, fixed values/constants, 
examples) and proven proper theorems (excl. automatically generated 
ones) by simple analysis of the sources, without running the system.

For Mizar/MML, my approach would be to look at tokens in .miz files and 
count:

For definitions: "definition"

For theorems: "theorem" and "scheme"


Does this sound reasonable? I am missing something? Any hints are 
appreciated.


Best,

Fabian Huch