src/HOL/Library/Code_Real_Approx_By_Float.thy
changeset 45771 a70465244096
parent 45496 5c0444d2abfe
child 46530 d5d14046686f