src/HOL/ex/Dedekind_Real.thy
changeset 40703 d1fc454d6735
parent 39910 10097e0a9dbd
child 40822 98a5faa5aec0