src/HOL/Real/real_arith.ML
changeset 26939 1035c89b4c02
parent 24093 5d0ecd0c8f3c
child 27545 7165068bb61f
equal deleted inserted replaced
26938:64e850c3da9e 26939:1035c89b4c02