Return-Path: Delivery-Date: Received: from leopard.cs.byu.edu (no rfc931) by swan.cl.cam.ac.uk with SMTP (PP-6.5) outside ac.uk; Fri, 17 Jun 1994 09:27:25 +0100 Received: by leopard.cs.byu.edu (1.37.109.8/16.2) id AA26230; Fri, 17 Jun 1994 02:12:18 -0600 Sender: info-hol-request@lal.cs.byu.edu Errors-To: info-hol-request@lal.cs.byu.edu Precedence: bulk Received: from dworshak.cs.uidaho.edu by leopard.cs.byu.edu with SMTP (1.37.109.8/16.2) id AA26226; Fri, 17 Jun 1994 02:12:07 -0600 Received: from irafs1.ira.uka.de by dworshak.cs.uidaho.edu with SMTP (1.37.109.8/16.2) id AA23095; Fri, 17 Jun 1994 01:10:35 -0700 Received: from i80fs2.ira.uka.de (actually i80fs2) by irafs1 with SMTP (PP); Fri, 17 Jun 1994 10:05:48 +0200 Received: from ira.uka.de by i80fs2.ira.uka.de id <08936-0@i80fs2.ira.uka.de>; Fri, 17 Jun 1994 10:12:30 +0200 Date: Fri, 17 Jun 94 10:12:29 EDT From: reetz To: info-hol@cs.uidaho.edu Subject: how fast is hol90's function theorem? Message-Id: <"i80fs2.ira.938:17.05.94.08.12.36"@ira.uka.de> I need a fast function to get a certain collection of alreay stored theorems in HOL90.6. Normally, looking for a theorem "bla" in theory "bli", one uses theorem "bli" "bla"; However, I would like to know how fast is it's implementation to estimate whether it is worth to program my own data structure to find things even faster. Assume there are n theorems in theory "bli", how long taks theorem "bli" to look for a certain theorem "bla", e.g. O(n), O(log n) ? Ralf. val anonymous_hol_user_disclaimer = --`"if your only tool is a hammer, every problem looks like a nail!"`--; (* Ralf Reetz, reetz@ira.uka.de or reetz@informatik.uni-karlsruhe.de *)