Return-Path: <john.harrison-request@uk.ac.cam.cl>
Delivery-Date: 
Received: from ted.cs.uidaho.edu by swan.cl.cam.ac.uk with SMTP (PP-6.2);
          Thu, 19 Nov 1992 19:09:23 +0000
Received: by ted.cs.uidaho.edu (16.6/1.34) id AA01213;
          Thu, 19 Nov 92 10:01:44 -0800
Sender: info-hol-request@edu.uidaho.cs.ted
Errors-To: info-hol-request@edu.uidaho.cs.ted
Precedence: bulk
Received: from Maui.CS.UCLA.EDU by ted.cs.uidaho.edu (16.6/1.34) id AA01208;
          Thu, 19 Nov 92 10:01:35 -0800
Received: by maui.cs.ucla.edu (Sendmail 5.61d+YP/3.21) id AA25577;
          Thu, 19 Nov 92 10:00:55 -0800
Date: Thu, 19 Nov 92 10:00:55 -0800
From: austel@EDU.UCLA.CS (Vernon Austel)
Message-Id: <9211191800.AA25577@maui.cs.ucla.edu>
To: info-hol@edu.uidaho.cs.ted
Subject: estimating run-time


The HOL timer reports the number of ``intermediate theorems generated'' -
which seems to mean the number of times mk_thm is called.

Since it is a *timer*, is this value (or was it at some point in the past)
relevent for *timing*?  In scientific program one commonly uses the
the number of floating-point or vector operations to estimate run-time;
does mk_thm play a similar role for HOL?

Thanks
Vernon