src/HOL/Real/ferrante_rackoff.ML
changeset 21346 c8aa120fa05d
parent 21078 101aefd61aac
child 21588 cd0dc678a205
equal deleted inserted replaced
21345:a18e60f597b6 21346:c8aa120fa05d