Define an evaluating definition for Sturm sequences
This should define a computable version of Sturm sequences in HOL4 and prove an equivalence with John Harrison's non-computing version.
Edited by Heiko Becker
This should define a computable version of Sturm sequences in HOL4 and prove an equivalence with John Harrison's non-computing version.