src/HOL/Library/Code_Real_Approx_By_Float.thy
changeset 45853 cbb6f2243b52
parent 45496 5c0444d2abfe
child 46530 d5d14046686f