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