You might have an older version of HOL4. I don't know when this theorem was introduced but if it was in HOL4 9 and you have HOL4 8, that could explain it. If so, either switch to the latest version, or, if not possible, just copy paste the proof in your own script (with potential dependencies).
-- Vincent Aravantinos Analysis and Design of Dependable Systems fortiss GmbH <www.fortiss.org/en> Guerickestrasse 25 | 80805 Munich | Germany > Le 24 oct. 2014 à 18:16, Cvetan Dunchev <[email protected]> a écrit : > > 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
