src/HOL/ex/Dedekind_Real.thy
changeset 57077 5bc908e5bf42
parent 56544 b60d5d119489
child 57492 74bf65a1910a