src/HOL/Real/ferrante_rackoff.ML
changeset 22800 eaf5e7ef35d9
parent 22578 b0eb5652f210
child 23318 6d68b07ab5cf