src/HOL/Library/Code_Real_Approx_By_Float.thy
changeset 65389 6f9c6ae27984
parent 63355 7b23053be254
child 66147 9225370db5f0