On Wed, 20 Jul 2011, Florian Haftmann wrote:
On Wed, Jul 20, 2011 at 11:33 AM, Alexander Krauss kra...@in.tum.de
wrote:
Now my question is: What do we actually know when
HOL-Generate-HOLLight completes without error? Should the generated
file be compared with the version in the repository and
Hi all,
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.
http://isabelle.in.tum.de/reports/Isabelle/report/ed3813d5499d44f6be414a5f051e85f3
for the first
On Wed, Jul 20, 2011 at 11:33 AM, Alexander Krauss kra...@in.tum.de wrote:
Now my question is: What do we actually know when HOL-Generate-HOLLight
completes without error? Should the generated file be compared with the
version in the repository and should the test fail when they are not
Dear all,
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.
http://isabelle.in.tum.de/reports/Isabelle/report/ed3813d5499d44f6be414a5f051e85f3
for the first
On 07/20/2011 09:34 PM, Florian Haftmann wrote:
Dear all,
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.
