[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

[PVS-Help] turning off rewrite



I have a recursively defined relation named <= on a datatype which I don't 
want to use as a rewrite.  Following the definition of <= I declare

   AUTO_REWRITE- <= : [dty,dty -> bool]

But grind on sequents involving <= seems to diverge rewriting it:

   Warning: Rewriting depth = 50; Rewriting with <=

I tried (stop-rewrite "myTheoryname.<=") which yields

   classtableSig.<= is not an auto-rewrite

How do I determine the installed rewrites, and more importantly uninstall 
this one?