Return-Path: <John.Harrison-request@cl.cam.ac.uk>
Delivery-Date: 
Received: from cs.uidaho.edu (actually ted.cs.uidaho.edu !OR! info-hol-request@cs.uidaho.edu) 
          by swan.cl.cam.ac.uk with SMTP (PP-6.5) outside ac.uk;
          Wed, 14 Jul 1993 15:51:02 +0100
Received: by cs.uidaho.edu (16.6/2.0) id AA03923; Wed, 14 Jul 93 07:41:47 -0700
Sender: info-hol-request@cs.uidaho.edu
Errors-To: info-hol-request@cs.uidaho.edu
Precedence: bulk
Received: from ULTRASTAR.EE.CORNELL.EDU by cs.uidaho.edu (16.6/2.0) id AA03918;
          Wed, 14 Jul 93 07:41:40 -0700
Received: by ultrastar.EE.CORNELL.EDU (4.1/1.6.10+n-y-Cornell-Electrical-Engineering) 
          id AA10979; Wed, 14 Jul 93 10:42:05 EDT
Message-Id: <9307141442.AA10979@ultrastar.EE.CORNELL.EDU>
From: markaa@ultrastar.EE.CORNELL.EDU (Mark D. Aagaard)
Date: Wed, 14 Jul 1993 10:42:04 -0400
Organization: Cornell University, Electrical Engineering, Ithaca NY 14853
X-Address: 389 Engineering and Theory Center
X-Phone: (607) 255 0302
X-Fax: (607) 255 9072
X-Mailer: Mail User's Shell (7.2.4 2/2/92)
To: info-hol@cs.uidaho.edu
Subject: kgs of proofs??

Does anyone have any statistics, estimates,
or guesses on the lines of code, number of 
proofs, kg of specification, etc produced
in/for/by HOL? I realize that this is a 
difficult thing to quantify, but any useful
information along these lines would be helpful.

 thanks in advance,

  -mark aagaard