src/HOL/Real.thy
changeset 81839 ea0c7189b15b
parent 80732 3eda814762fc