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

Re: 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?
> 
> Thanks,
> Hanne

GRIND has a large number of options, you can read about them using
C-c C-h c grind (or M-x help-pvs-prover-command grind).  What you probably
want is something like

(grind :theories ("mytheory") :exclude ("mydef" "myifflemma"))

Regards,

Sam Owre <Owre@csl.sri.com>
Computer Science Lab, SRI International   Tel: (650) 859-5114              
333 Ravenswood Avenue                     FAX: (650) 859-2844              
Menlo Park, CA  94025 USA