src/HOL/Library/Code_Real_Approx_By_Float.thy
changeset 65946 5dd3974cf0bc
parent 63355 7b23053be254
child 66147 9225370db5f0