src/HOL/RealDef.thy
changeset 41731 2fb760843e17
parent 41550 efa734d9b221
child 41792 ff3cb0c418b7
equal deleted inserted replaced
41730:14ed42540d22 41731:2fb760843e17