src/HOL/Real.thy
changeset 35437 fe196f61b970
parent 35090 88cc65ae046e
child 36899 bcd6fce5bf06
equal deleted inserted replaced
35422:e74b6f3b950c 35437:fe196f61b970