src/HOL/Real/ROOT.ML
changeset 5418 a895ab904b85
parent 5078 7b5ea59c0275
child 5588 a3ab526bb891