src/HOL/RealDef.thy
changeset 30501 3e3238da8abb
parent 30242 aea5d7fa7ef5
child 31100 6a2e67fe4488
equal deleted inserted replaced
30491:772e95280456 30501:3e3238da8abb