src/HOL/Library/Code_Real_Approx_By_Float.thy
changeset 45615 c05e8209a3aa
parent 45496 5c0444d2abfe
child 46530 d5d14046686f