src/HOL/Library/Float.thy
changeset 45405 23e5af70af07
parent 44766 d4d33a4d7548
child 45495 c55a07526dbe