src/HOL/Real.thy
changeset 61825 69b035408b18
parent 61799 4cf66f21b764
child 61942 f02b26f7d39d