src/HOL/Library/Code_Real_Approx_By_Float.thy
changeset 66787 64b47495676d
parent 66148 5e60c2d0a1f1
child 67399 eab6ce8368fa