src/HOL/Library/Code_Real_Approx_By_Float.thy
changeset 51595 8e9746e584c9
parent 51542 738598beeb26
child 52403 140ae824ea4a