Re: [mizar] referring to unlabeled theorems

[Artur Kornilowicz <arturk@math.uwb.edu.pl>]

On Sat, 17 Feb 2007, Jesse Alama wrote:

> I'm trying to use FVSUM_1:22 in a proof I'm working on, but I get
> error *192 ("Inaccessible theorem") when doing so.  The problem seems
> to be that the twenty-second theorem of FVSUM_1 is not labeled as
> such, even though the semantic presentation of FVSUM_1 does assign a
> label to this theorem.  How can I refer to this theorem?
>
> Thanks,
>
> Jesse

Hi Jesse,

I assume you have FVSUM_1 in your directive 'theorems'.

*192 is also reported when some constructors are missed to understand a 
theorem. You can find it out calling

constr -f text/filename fvsum_1:22

Best
Artur