src/HOL/Library/Float.thy
changeset 45615 c05e8209a3aa
parent 45495 c55a07526dbe
child 45772 8a8f78ce0dcf