Home Intro Announce FAQ Docs Download Mail Status Bugs Users Related FM Tools

PVS Bug 676


Synopsis:        Enahancement request: Selective unlabeling feature
Severity:        serious
Priority:        medium
Responsible:     owre
State:           open
Class:           sw-bug
Arrival-Date:    Thu Jun 13 03:35:00 2002
Originator:      Tamarah Arons
Organization:    wisdom.weizmann.ac.il
Release:         PVS 2.4
Environment: 
 System:          
 Architecture: 

Description: 
  Hello,
  
  I would very much appreciate the ability to unlabel one label, and not all
  labels from a formula.
   
  E.g. given a sequent formula 
    
    {-1,(templabel inv)} 
        p!1 = q!1
    
  in the sequents I would like to be able to remove the label "templabel"
  while retaining "inv". (unlabel "templabel") removes both.
    
  My motivation is that when writing strategies I would like to temporarily
  label some lines, which may move during the strategy, and then remove the 
  labeling before completing the strategy. 
  Currently, such strategies either leave the temporary labeling, or remove 
  it at the cost of destroying pre-existing labeling.
  
  Thanks,
  Tamarah
  

How-To-Repeat: 

Fix: 
Home Intro Announce FAQ Docs Download Mail Status Bugs Users Related FM Tools