Jon, 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'={}! Roger _______________________________________________ Proofpower mailing list Proofpower@lemma-one.com http://lemma-one.com/mailman/listinfo/proofpower_lemma-one.com