src/HOL/Library/Float.thy
changeset 43244 db041e88a805
parent 42676 8724f20bf69c
child 44766 d4d33a4d7548