src/HOL/Real/ROOT.ML
changeset 8862 78643f8449c6
parent 8856 435187ffc64e
child 9000 c20d58286a51