[Date Prev][Date Next]
[Chronological]
[Thread]
[Top]
Re: [mizar] referring to unlabeled theorems
On Sat, 17 Feb 2007, Jesse Alama wrote:
One thing that annoys me slightly is that the .miz form of a MIZAR
article doesn't necessarily have labels for all theorems. I prefer to
look at MIZAR articles (not abstracts) in emacs, and sometimes I find
an unlabeled theorem that I want to use. In these situations I have
to look at, e.g., the semantic presentation of that article or the
abstract to find out how to refer to that theorem. It would be nice
if theorems in .miz files were labeled as they are in the abstracts
and the semantic presentation.
It's because all articles are as a rule cleansed of all unnecessary
labels, i.e statements not referred to in the current article shouldn't be
labelled. Theorems are no exception here.
Best,
Adam Naumowicz
======================================================================
Department of Applied Logic fax. +48 (85) 745-7662
Institute of Computer Science tel. +48 (85) 745-7559 (office)
University of Bialystok e-mail: adamn@mizar.org
Sosnowa 64, 15-887 Bialystok, Poland http://math.uwb.edu.pl/~adamn/
======================================================================