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 hol-info@lists.sourceforge.net https://lists.sourceforge.net/lists/listinfo/hol-info
