Exporter

Overview

Exporter separates reusable knowledge from a Mizar Article and prepaires it for storage in the data base.

Usage

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

Technical Details

Usually, exporter is called within the miz2prel(or miz2prel.bat) user script to produce a local data base. Extracted data is kept within a subdirectory prel in the current directory.
[ Home | Project | Language | System | People | MML | FM | SUM ]

Last modified: April 9, 2010