I think the problem now is that the syntactic form of the HOL term you
supply to 'new_inductive_definition' does not fit what is allowed by the
command, because you are not allowed to have compound implications (see
the HOL Light reference manual entry for 'new_inductive_definition').
So I think y
Hello,
On 06/16/2016 01:45 PM, Mark Adams wrote:
Hi Heiko,
That's strange, your corrected version goes through fine on my
computer. Do you still get the same problem if you restart HOL Light
and enter the corrected script? What version of HOL Light are you using?
Mark.
It turns out,
