src/HOL/Library/Code_Real_Approx_By_Float.thy
changeset 64588 293ab573d034
parent 63355 7b23053be254
child 66147 9225370db5f0