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