src/HOL/Real.thy
changeset 76453 2ba80c2fc325
parent 75864 3842556b757c
child 77490 2c86ea8961b5
equal deleted inserted replaced
76452:220f6f377d52 76453:2ba80c2fc325