src/HOL/Real/ROOT.ML
changeset 6701 e84a0b941beb
parent 6490 4961ecbaaff7
child 7219 4e3f386c2e37