src/HOL/Real/ferrante_rackoff_proof.ML
changeset 22999 c1ce129e6f9c
parent 22997 d4f3b015b50b
child 23021 f602a131eaa1