I am not sure what the problem is: have you done an open pred_setTheory;
? On my machine, the theorem is there: > $hol > > --------------------------------------------------------------------- > HOL-4 [Kananaskis 9 (stdknl, built Wed Oct 22 13:44:55 2014)] > > For introductory HOL help, type: help "hol"; > To exit type <Control>-D > --------------------------------------------------------------------- > > Poly/ML 5.5.2 Testing > > pred_setTheory.CROSS_applied; > val it = > |- ∀P Q x. (P × Q) x ⇔ FST x ∈ P ∧ SND x ∈ Q: > thm Konrad. On Fri, Oct 24, 2014 at 11:16 AM, Cvetan Dunchev <[email protected]> wrote: > Dear colleagues and friends, > > I would like to inform you about the following problem: I want to use > the CROSS_applied theorem from the pred_setTheory: > > > http://hol.sourceforge.net/kananaskis-9-helpdocs/help/src-sml/htmlsigs/pred_setTheory.html#CROSS_applied-val > > Despite the fact that the theory is loaded, I got the following > message in the console: > ! Toplevel input: > ! CROSS_applied; > ! ^^^^^^^^^^^^^ > ! Unbound value identifier: CROSS_applied > > and when I have a look at the corresponding source file, indeed such a > theorem does not exist. Does anybody have an explanation about that? > > Best regards, > Cvetan Dunchev > > > > ------------------------------------------------------------------------------ > _______________________________________________ > hol-info mailing list > [email protected] > https://lists.sourceforge.net/lists/listinfo/hol-info >
------------------------------------------------------------------------------
_______________________________________________ hol-info mailing list [email protected] https://lists.sourceforge.net/lists/listinfo/hol-info
