On Sat, Mar 5, 2016 at 3:04 AM, Michael Norrish
wrote:
> I turned the simplifier trace on to see the following steps taken:
The simplifier trace looks really nice! How do I turn it on? I do not
see this in the documentation...
-
Hi,guys
I had resolved this question. I substituted src file in
https://github.com/HOL-Theorem-Prover/HOL for src in HOL4 directory, and start
HOL4 by pointing hol\bin\hol.bat. Then, it worked.
Message: 2
Date: Wed, 2 Mar 2016 10:18:04 +0800
From: " ?? " <956066...@qq.com>
Subjec
Section 6.2 (The Trace System) of the Description manual describes the
trace system.
Interactively, the functions traces and set_trace may be of interest. I
think the simplifier trace is called "simplifier".
On 6 March 2016 at 01:16, Piotr Trojanek wrote:
> On Sat, Mar 5, 2016 at 3:04 AM, Micha
