Additional information. I suspected that this behavior may be due to a
poorly handled out of memory situation. On a system configured with
more memory, I see a different error.
.
val EXPAND_QUANTS_CONV : thm -> conv =
- : unit = ()
- : unit = ()
module type Arith_float_sig =
sig
val
Package: hol-light
Version: 20170109-1
Severity: normal
Dear Maintainer,
*** Reporter, please consider answering these questions, where appropriate ***
* What led up to the situation?
$ cd /usr/share/hol-light/Formal_ineqs
$ hol-light
...hol-light starts up and presents prompt #...
# needs
2 matches
Mail list logo
