src/HOL/ex/Dedekind_Real.thy
changeset 48759 ff570720ba1c
parent 47108 2a1953f0d20d
child 49834 b27bbb021df1
equal deleted inserted replaced
48749:c197b3c3e7fa 48759:ff570720ba1c