Exporter separates reusable knowledge from a Mizar Article and prepaires it for storage in the data base.
exporter [options] article-file-name [environment-name]
Options: -q Suppress output of running line numbers and errors -l Allow for source lines longer than 80 characters
exporteris called within the
miz2prel.bat) user script to produce a local data base. Extracted data is kept within a subdirectory
prelin the current directory.
Last modified: April 9, 2010