src/HOL/RealDef.thy
changeset 45770 5d35cb2c0f02
parent 45184 426dbd896c9e
child 45818 53a697f5454a
equal deleted inserted replaced
45769:2d5b1af2426a 45770:5d35cb2c0f02