src/HOL/ex/Dedekind_Real.thy
changeset 54667 4dd08fe126ba
parent 53373 3ca9e79ac926
child 54230 b1d955791529