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; Thu, 13 Jan 1994 15:37:54 +0000 Received: by leopard.cs.byu.edu (1.37.109.8/16.2) id AA01078; Thu, 13 Jan 1994 08:17:51 -0700 Sender: info-hol-request@leopard.cs.byu.edu Errors-To: info-hol-request@leopard.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 AA01074; Thu, 13 Jan 1994 08:17:35 -0700 Received: from swan.cl.cam.ac.uk by dworshak.cs.uidaho.edu with SMTP (1.37.109.8/16.2) id AA24624; Thu, 13 Jan 1994 07:15:18 -0800 Received: from cormorant.cl.cam.ac.uk (user mjcg (rfc931)) by swan.cl.cam.ac.uk with SMTP (PP-6.5) to cl; Thu, 13 Jan 1994 15:14:07 +0000 Received: by cormorant.cl.cam.ac.uk (4.1/SMI-3.0DEV3) id AA19208; Thu, 13 Jan 94 15:13:39 GMT Date: Thu, 13 Jan 94 15:13:39 GMT From: Mike.Gordon@cl.cam.ac.uk Message-Id: <9401131513.AA19208@cormorant.cl.cam.ac.uk> To: info-hol@cs.uidaho.edu Subject: In praise of Mosaic This message is to futher praise Phil Windley's amazing hypertext documentation system for HOL. Just now I was in the middle of a horrible proof about Z schemas. IMP_RES_TAC was generating too many assumptions. I vaguely remembered that there had been some correspondence on info-hol about this, so I fired up Mosaic, selected "Dynamic Search of INFO-HOL Messages" (one click), did a keyword search for "Resolution" and got: Nicer resolution Ching Tsun Chou (May 31, 1993) Re: Nicer resolution Tom Melham (May 31, 1993) More on HOL improvement: Resolution Ching Tsun Chou (Sep 06, 1993) modified resolution functions David Shepherd (Sep 21, 1993) Resolution with filters Ching Tsun Chou (Sep 25, 1993) I looked in the second and third of these (1 click each), found the tactic code I wanted in Ching Tsun's message and cut-and-pasted it into my file ... and my problem was solved in just a few minutes. Thank you Phil (and also Ching Tsun)! Mike