<!DOCTYPE HTML PUBLIC "-//W3C//DTD HTML 4.01 Transitional//EN">
<html>
<head>
<meta content="text/html; charset=ISO-8859-1"
http-equiv="Content-Type">
<title></title>
</head>
<body text="#000000" bgcolor="#ffffff">
On 07/20/2011 09:34 PM, Florian Haftmann wrote:
<blockquote cite="mid:4E272DDE.7000803@informatik.tu-muenchen.de"
type="cite">
<pre wrap="">Dear all,
</pre>
<blockquote type="cite">
<pre wrap="">with Cezary's guidance, I set up mira configurations for building the
proofs bundle from the HOL Light repository and for running the
HOL-Generate-HOLLight with that bundle, cf.
<a class="moz-txt-link-freetext" href="http://isabelle.in.tum.de/reports/Isabelle/report/ed3813d5499d44f6be414a5f051e85f3">http://isabelle.in.tum.de/reports/Isabelle/report/ed3813d5499d44f6be414a5f051e85f3</a>
for the first successful run. I experienced some fairly reproducible
segmentation faults on some machines, but lxbroy5-9 seem to work. This
is still prior to Cezary's major cleanup in 6ca79a354c51, so there is
hope for improvements here.
</pre>
</blockquote>
<pre wrap="">
these are good news, thanks for the excellent work that is going on!
A humble question: is there any chance that also the HOL4 import can be
covered?
</pre>
</blockquote>
As we discussed at lunch in Munich, we have an expert on HOL4,
Thomas Tuerk, who might take that opportunity.<br>
<br>
Lukas<br>
<br>
<blockquote cite="mid:4E272DDE.7000803@informatik.tu-muenchen.de"
type="cite">
<pre wrap="">Cheers,
Florian
</pre>
<pre wrap="">
<fieldset class="mimeAttachmentHeader"></fieldset>
_______________________________________________
isabelle-dev mailing list
<a class="moz-txt-link-abbreviated" href="mailto:isabelle-dev@in.tum.de">isabelle-dev@in.tum.de</a>
<a class="moz-txt-link-freetext" href="https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev">https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev</a>
</pre>
</blockquote>
<br>
</body>
</html>