Re: [isabelle] solving an equation in isabelle


> the important things in the equation are :
> (((y1-y2)^nat (p - 3)) - x1 ) ^3 = .....

There is a new mthod (not yet included in the repository) to solve similar 
problems based on Groebner bases. Yet I do'nt think that it would work for 
these instances. The key questions are:
a) is nat a variable?
b) can you get rid of substraction (-) in your context

If the answer to both is yes, then the method would work for you. 
Unfortunately It might take time to include it.

Otherwise try stuff like ring_eq_simps and add appropriate theorems for 


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