src/HOL/Library/Code_Real_Approx_By_Float.thy
changeset 68575 d40d03487f64
parent 67399 eab6ce8368fa
child 69064 5840724b1d71