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

PVS Bug 934


Synopsis:        feature wish: mark lhs, rhs and condition in auto rewrite list
Severity:        serious
Priority:        medium
Responsible:     owre (Sam Owre)
State:           open
Class:           sw-bug
Arrival-Date:    Tue Jan 24 11:35:00 2006
Originator:      Hendrik Tews
Organization:    tcs.inf.tu-dresden.de
Release:         PVS 3.2
Environment: 
 System:          
 Architecture: 

Description: 
  Hi,
  
  it would be nice if, in the list produced by 
  M-x show-auto-rewrites, one could see what PVS considers as left
  hand side, right hand side and condition of each rule.
  
  A common error is that a lemma does not fulfill the requirements
  for auto rewrites and, thus the whole lemma is taken as an atomic
  boolean auto-rewrite. With the new featue one could easily see
  this.
  
  
  Bye,
  
  Hendrik

How-To-Repeat: 

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