src/HOL/Real.thy
changeset 56159 39f7b7690de6
parent 56078 624faeda77b5
child 56217 dc429a5b13c4
equal deleted inserted replaced
56158:c2c6d560e7b2 56159:39f7b7690de6