src/HOL/ex/Dedekind_Real.thy
changeset 51635 e8e027aa694f
parent 49962 a8cc904a6820
child 53215 5e47c31c6f7c