src/HOL/Library/Code_Real_Approx_By_Float.thy
changeset 78425 62d7ef1da441
parent 75800 a21debbc7074
child 81706 7beb0cf38292
equal deleted inserted replaced
78424:e5908be41a36 78425:62d7ef1da441