src/HOL/Library/Code_Real_Approx_By_Float.thy
changeset 65170 53675f36820d
parent 63355 7b23053be254
child 66147 9225370db5f0