src/HOL/Real.thy
changeset 57365 d2090a01e920
parent 57275 0ddb5b755cdc
child 57447 87429bdecad5
equal deleted inserted replaced
57364:c1060d10089f 57365:d2090a01e920