src/HOL/Real/RealArith.thy
changeset 13816 cc228bd9c1fc
parent 10722 55c8367bab05
child 14269 502a7c95de73
equal deleted inserted replaced
13815:0832792725db 13816:cc228bd9c1fc