Re: [Hol-info] useful HOL statistics to show the amount of proof work?

[Lu Z. <lu...@cs...>]

> I would like to know how we can collect these information, I mean the
> run time, gctime, and primitive inference steps and so on, especially in

I found out in Count.sml that there are other utilities available, too. 
For example, you can use the following to start counting:

val meter = Count.mk_meter();

and use

Count.report(Count.read meter);

to see the statistics, after whatever operations you do.

Best,
Lu