----------------------------------------------------------------------
thm_count                                                      (Count)
----------------------------------------------------------------------
thm_count :
     unit ->
     {ASSUME : int, REFL : int, BETA_CONV : int, SUBST : int,
      ABS : int, DISCH : int, MP : int, INST_TYPE : int,
      MK_COMB : int, AP_TERM : int, AP_THM : int, ALPHA : int,
      ETA_CONV : int, SYM : int, TRANS : int, EQ_MP : int,
      EQ_IMP_RULE : int, INST : int, SPEC : int, GEN : int,
      EXISTS : int, CHOOSE : int, CONJ : int, CONJUNCT1 : int,
      CONJUNCT2 : int, DISJ1 : int, DISJ2 : int, DISJ_CASES : int,
      NOT_INTRO : int, NOT_ELIM : int, CCONTR : int, GEN_ABS : int,
      definition : int, axiom : int, from_disk : int, oracle :int,
      total :int }

SYNOPSIS
Returns the current value of the theorem counter.

DESCRIBE
If enabled, HOL maintains a counter which is incremented every time a
primitive inference is performed (or an axiom or definition set up). A
call to {thm_count()} returns the current value of this counter.
Inference counting needs to be enabled with the call
{Count.counting_thms true}.  Counting can be turned off by calling
{counting_thms false}.

The default is for inference counting not to be enabled.

FAILURE
Never fails.

SEEALSO
Count.apply.

----------------------------------------------------------------------