Hi,
I believe this is due to how hol-mode copies input from emacs buffers to
HOL. Look at HOL-DIR/tools/hol-mode.el line 802 ff.
(https://github.com/HOL-Theorem-Prover/HOL/blob/master/tools/hol-mode.src#L800).
If a chunk of text you want to send exceeds a certain size, it is
written to a
Hi,
I'm trying to use the tactical SPLIT_LT to multiple subgoals. However, I'm
facing error with assumption matching. For instance, I've a proof goal of
this form:
`(A1 ==> B1) ==> (B1 /\ SG2 /\ SG3)`
rw []
\\ (pop_assum (fn th => match_mp_tac th)) THEN_LT SPLIT_LT 1 (ALL_LT,
ALLGOALS (rw[]))
Hi,
thank you for your reply.
I am using an oracle virtual machine on my laptop
running ubuntu-16.04.4-desktop-i386. I have been using this machine for
about three months now, and I have not had any problem until yesterday.
Best Regards,
Yassmeen
On Thu, Sep 20, 2018 at 5:25 PM, Thomas Tuerk
Hi,
Thanks for the reply. I think the match_mp_tac is causing the error since
if I only pop the assumption the tactic works on first subgoal.
rw [] \\ (pop_assum (mp_tac)) THEN_LT SPLIT_LT 1 (ALL_LT, ALLGOALS (rw[]))
> val it =
SG3
A1 ==> B1
Seems like the rw[] is breaking the proof into 3 subgoals, and only on the
first one is the pop_assum match_mp_tac succeeding. So the proof is failing
before it gets to the THEN_LT.
Konrad.
On Thu, Sep 20, 2018 at 2:05 PM Waqar Ahmad via hol-info <
hol-info@lists.sourceforge.net> wrote:
> Hi,
**
The 22nd International Conference on
Logic for Programming, Artificial Intelligence and Reasoning
LPAR-22
Haile Resort,
Hi,
I am using HOL4 in hol-mode, yesterday I started receiving this error
message
___
hol-info mailing list
hol-info@lists.sourceforge.net
https://lists.sourceforge.net/lists/listinfo/hol-info
Hi,
Sorry for sending this email again, but it seems that there was a problem
with the first email
I am using HOL4, yesterday I started receiving this error message
Exception raised Io {cause = SysErr ("No such file or directory", SOME
ENOENT), function = "TextIO.openIn", name =
