src/HOL/Real.thy
changeset 68664 bd0df72c16d5
parent 68662 227f85b1b98c
child 68669 7ddf297cfcde