src/HOL/Library/Code_Real_Approx_By_Float.thy
changeset 51618 a3577cd80c41
parent 51542 738598beeb26
child 52403 140ae824ea4a