Dear friends, thanks a lot for your help!
Indeed my version is old: I am using version 7.0 of HOL4, because I work on old scripts. I will do what Vincent suggested. The problem is solved ! :) Best regards, Cvetan Dunchev Quoting Anthony Fox <[email protected]>: > The theorem comes from a custom version of store_thm, which was > added in November 2012. See: > > https://github.com/HOL-Theorem-Prover/HOL/commit/1de5add5520bcd6bc6b44258e5a3d881d5bb9a4c > > It appears that this didn?t make it to the HOL4 K-8 release. > > Anthony > >> On 25 Oct 2014, at 17:09, Vincent Aravantinos >> <[email protected]> wrote: >> >> 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 > > ------------------------------------------------------------------------------ _______________________________________________ hol-info mailing list [email protected] https://lists.sourceforge.net/lists/listinfo/hol-info
