src/HOL/Real/real_arith.ML
changeset 10712 351ba950d4d9
parent 10693 9e4a0e84d0d6
child 10722 55c8367bab05
equal deleted inserted replaced
10711:a9f6994fb906 10712:351ba950d4d9