Return-Path: Return-Path: Received: from iris.eecs.ucdavis.edu by swan.cl.cam.ac.uk with SMTP (PP) to cl id <20245-0@swan.cl.cam.ac.uk>; Thu, 3 Oct 1991 10:17:59 +0100 Received: by iris.eecs.ucdavis.edu (5.57/UCD.EECS.7.0) id AA08530; Thu, 3 Oct 91 02:07:01 -0700 Received: from esat.kuleuven.ac.be by n-kulcs.cs.kuleuven.ac.be (5.65b/n_kulcs1.1) id AA04926; Thu, 3 Oct 91 11:07:24 +0200 Date: Thu, 3 Oct 91 10:08:03-0100 Message-Id: <9110031008.AA12881@esat.kuleuven.ac.be> Received: by esat.kuleuven.ac.be Thu, 3 Oct 91 10:08:06-0100 From: ploegaer@be.imec To: info-hol@iris.ucdavis.edu Subject: library auxiliary, 3rd trial sorry if you already got this, but I have the impression it did not get through ... ----------------------------------------------------------------------- Hi! I'm currently writing the documentation for the library `auxiliary`. As several of the tactics supplied by `auxiliary` are good examples of a bad proof style (proof: problems with porting the libraries well-order and zet to version 1.12), we think about `rewriting` auxiliary ... > From: gpx3u::Tom.Melham@cl.cam.ac.uk > Personally, I would like to see the auxiliary library discontinued all > together. It's basically Ton's personal environment, and not really > suitable for a library. But it's best to send a message out to info-hol, Thus, if you are using the library `auxiliary`, please let me know (ASAP!) which functions you are using. The `dangerous` features will be removed (completely) if nobody uses them, else they might be put in the contrib or some of these even kept in the library!! All libraries depending on the tactics from `auxiliary` will be/have been rewritten. If you are only using these libraries you don't have to fear anything. (you won't `see` the changes) Wim Ploegaerts ---------------------------------------------------------------------- Ploegaerts Wim e-mail: ploegaer@imec.be Imec vzw. Tel.: (32) 16/281 525 Kapeldreef 75 Fax.: (32) 16/281 515 3001 Leuven, Belgium Telex: 26.152