[isabelle] Isabelle, Diophantine equations

  could someone please tell me how to handle Diophantine equations in Isabelle and
  give me some simple example?
  For example how to try to prove or disprove
     all x, exits y, x^4=y^2
     exists x, exists y, x^4 = 1 + x + y^2
     exists x, exists y, x^2 (1 + y) = 1 + x + y^2
  Thank you, Jan Pax

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