Return-Path: Received: from ted.cs.uidaho.edu by swan.cl.cam.ac.uk with SMTP (PP-6.0) id <18228-0@swan.cl.cam.ac.uk>; Thu, 7 May 1992 15:03:26 +0100 Received: by ted.cs.uidaho.edu (16.6/1.34) id AA11367; Thu, 7 May 92 06:41:47 -0700 Sender: info-hol-request@edu.uidaho.cs.ted Errors-To: info-hol-request@edu.uidaho.cs.ted Received: from utrhcs.cs.utwente.nl by ted.cs.uidaho.edu (16.6/1.34) id AA11363; Thu, 7 May 92 06:41:39 -0700 Received: from perseus.cs.utwente.nl by utrhcs.cs.utwente.nl (4.1/RBCS-2.2mx) id AA13347; Thu, 7 May 92 14:58:14 +0200 Received: from utis60.cs.utwente.nl by perseus.cs.utwente.nl (4.1/RBCS-2.0) id AA03694; Thu, 7 May 92 14:58:12 +0200 Date: Thu, 7 May 92 14:58:12 +0200 From: vdvoort@nl.utwente.cs (Mark van de Voort) Message-Id: <9205071258.AA03694@perseus.cs.utwente.nl> To: info-hol@edu.uidaho.cs.ted Subject: discarding theory segments Maybe I'm missing the obvious, but is there any function which allows me to discard the whole current theory-segment? (but keeps ml-functions which have been introduced) This would be handy during testing. As it is now I have to make up new names for definitions and theorems when a previous (automatic) definition went slightly wrong. If this is impossible, because my code relies on some strict naming scheme, I have to quit the session and reload everything. I think it is logically sound to discard the latest segment, so I so no reasons not to have such a function Regards, Mark.