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
