subject:"\[Hol\-info\] CROSS_applied thm."

Re: [Hol-info] CROSS_applied thm.

2014-10-25 Thread Konrad Slind

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

Re: [Hol-info] CROSS_applied thm.

2014-10-25 Thread Vincent Aravantinos

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).