src/HOL/ex/Dedekind_Real.thy
changeset 49081 092668a120cc
parent 47108 2a1953f0d20d
child 49834 b27bbb021df1