Return-Path: Return-Path: Received: from ted.cs.uidaho.edu by swan.cl.cam.ac.uk with SMTP (PP-6.0) id <19143-0@swan.cl.cam.ac.uk>; Wed, 19 Feb 1992 21:48:53 +0000 Received: by ted.cs.uidaho.edu (16.6/1.34) id AA11979; Wed, 19 Feb 92 13:18:15 -0800 Sender: info-hol-request@edu.uidaho.cs.ted Errors-To: info-hol-request@edu.uidaho.cs.ted Received: from sparta.oracorp.com by ted.cs.uidaho.edu (16.6/1.34) id AA11975; Wed, 19 Feb 92 13:17:53 -0800 Date: Wed, 19 Feb 92 16:18:59 EST From: shb@com.oracorp.sparta Received: by sparta.oracorp.com (4.1/1.3-ORA Corporation) id AA08757; Wed, 19 Feb 92 16:18:59 EST Message-Id: <9202192118.AA08757@sparta.oracorp.com> To: info-hol@edu.uidaho.cs.ted Subject: Sorting utility I've written a C utility that can take files of HOL items delimited by parentheses (e.g., lists produced by "axioms" or "theorems") or by double-quote characters (e.g., the typed constants produced with other things by "print_theory") and produce files of these items separated by single spaces and sorted alphabetically. These files are very useful when one has to look up something that's used in a prover session produced by someone else. If there's anyone else out there who's having to deal with large numbers of HOL constants, axioms, and definitions written by someone else, and who'd like to have this utility, I'd be happy to provide it and any additional information needed to use it. Steve Brackin ORA Corporation