Return-Path: <John.Harrison-request@cl.cam.ac.uk>
Delivery-Date: 
Received: from leopard.cs.byu.edu (no rfc931) by swan.cl.cam.ac.uk 
          with SMTP (PP-6.5) outside ac.uk; Wed, 17 Aug 1994 04:08:44 +0100
Received: by leopard.cs.byu.edu (1.37.109.8/16.2) id AA12923;
          Tue, 16 Aug 1994 21:03:24 -0600
Sender: info-hol-request@lal.cs.byu.edu
Errors-To: info-hol-request@lal.cs.byu.edu
Precedence: bulk
Received: from SAIL.Stanford.EDU by leopard.cs.byu.edu 
          with SMTP (1.37.109.8/16.2) id AA12919;
          Tue, 16 Aug 1994 21:03:23 -0600
Received: by SAIL.Stanford.EDU (5.57/25-eef) id AA23453;
          Tue, 16 Aug 94 19:59:20 -0700
Date: Tue, 16 Aug 94 19:59:20 -0700
From: "P." Sreeranga Rajan <sreerang@SAIL.Stanford.EDU>
Message-Id: <9408170259.AA23453@SAIL.Stanford.EDU>
To: info-hol@leopard.cs.byu.edu
Subject: timings: Tamarack-{2,3} in HOL
Cc: sreerang@SAIL.Stanford.EDU


For a statistical data point, I am interested in knowing how long
it took for someone to specify and verify Tamarack-{2,3} in HOL.
[It surely would depend on experience in using HOL.]

Thanks,
Sree
----