Re: [isabelle] unexpected (for me) output using FOL



The collapsing of ALL x. P(x) to All(P) is a side-effect of the way that all binding syntax is handled in Isabelle. Although it can be annoying, here All(P)-->All(P) tells you that (ALL x. P(x)) and (ALL y. P(y)) are actually the same formula in Isabelle.

Larry Paulson


On 3 Nov 2006, at 01:03, Joao Marcos wrote:

Level 0 (1 subgoal)
((ALL x. P(x))<->(ALL y. P(y)))
1. ((All(P)-->All(P))&(All(P)-->All(P)))

WHY??






This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.