src/HOL/Library/Code_Real_Approx_By_Float.thy
changeset 63426 2e4de628201f
parent 63355 7b23053be254
child 66147 9225370db5f0