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.
On 16/06/2016 10:01, Heiko Becker wrote:
> Forwarded Message --
Hello Heiko,
It worked for me:
let sstep_RULES,sstep_INDUCT,sstep_CASES = new_inductive_definition
`(!x e s env v. exp_eval e env = v ==> sstep (Ass x e s) env s
(upd_env x v env)) /\
(!c s t env. bval c env = T ==> sstep (Ite c s t) env s env) /\
(!c s t env. bval c env = F ==> sstep (I
Forwarded Message
Subject:Re: [Hol-info] HOL-Light Beginner Questions
Date: Thu, 16 Jun 2016 10:59:44 +0200
From: Heiko Becker
To: Ramana Kumar
CC: hol-info
On 06/16/2016 01:57 AM, Ramana Kumar wrote:
I expect it could be because the Boolean constants
