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

problem with prover

I have had problems with using the proof command 'expand'. Sometimes it
will not expand a definition when I believe it should. All it says is
e.g. 'no change on expand "index"', yet at other times it has expanded
the very same definition, e.g. "index". This has happened on numerous
occasions with various definitions. Unfortunately Ive no simple example.
Have you any information on this problem, or would you like me to send
an example?
Richard Botting                         tel: +44 141 339 8855 ext. 8335
Computing Science                      fax: +44 141 330 4913
University of Glasgow                email: rmb@dcs.gla.ac.uk
Glasgow G12 8QQ