XML for Mizar and MML See http://ktiml.mff.cuni.cz/~urban/mizxml.ps for description of Mizar XML-ization. See MizarXmlImplementation for implementation notes. Main ...
FunctorSynonyms The definition of dist(x,y) could be just a synonym. With appropriate clusters, the result type of (the distance of M).(x,y) is a real number already ...
An Attempt to Find Consensus about Indenting Rules for Mizar TOC Block Rules proof, now, hereby, suppose, case should increase indentation, end; should decrease ...
Let's document the discussion about Mizar structures St. like "strict-independence" (maybe property?) of some constructors would be quite useful; I am having the ...
How to do Computer Algebra in Mizar TOC Problem description Eventually, users will want to have things like inverse matrix for concrete 5x5 matrices quickly available ...
Mechanisms identifying, implying or interpreting theorems between intuitively "similar" notions should be discussed in general. As of the current Mizar, I would include ...
Related topics: WebHome, BrainstormScratchPad?, FeatureEnhancementRequests?, FeatureToDo?, FeatureUnderConstruction?, FeatureDone?, FeatureNotSuitable? to top