[isabelle] Isabelle, Diophantine equations



  Hi,
  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.