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

[PVS-Help] 'divides' definition

How can I use 'use' or 'lemma' to introduce an instance of the
'divides' definition from theory divides in the prelude?  I've tried 

(lemma divides (n "L" m "L")) and
(lemma divides (n "L")) 
and some others and was given the message:

	"Found 2 resolutions for divides relative to the substitution.
	Please check substitution, provide actual parameters for lemma
	name, or supply more substitutions."

Thanks,
Rob