src/HOL/Library/Float.thy
changeset 80645 a1dce0cc6c26
parent 80452 0303b3a0edde
child 80732 3eda814762fc
equal deleted inserted replaced
80644:6a996ad11af2 80645:a1dce0cc6c26