On Saturday 22 Sep 2012 00:11, Jon Lockhart wrote:

> I tried what you mentioned after Phil brought it up and
> if you try to do State' and then push' = {} the system
> throws an error saying "No free types allowed in
> predicates" which to me means that push is not
> accessible in the predicate section.

Should be pushed'={}!


Proofpower mailing list

Reply via email to