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

using grind

I want to use grind with a theory. The theory consists of a definition
(which I don't want to expand), a lemma with an IFF statement (which I
don't want to use either) and a whole lot of lemmas concerning
implications (which I do want to use).

Apart from splitting the theory up, is there any way of doing this?


Hanne Gottliebsen		    Office P337
Dept. of Computer Science	    Ph: +44 1334 46 3265
University of St Andrews	    hago@dcs.st-and.ac.uk
                   - Who moved the stone?