src/HOL/ex/Dedekind_Real.thy
changeset 55885 c871a2e751ec
parent 54863 82acc20ded73
child 56544 b60d5d119489
equal deleted inserted replaced
55884:f2c0eaedd579 55885:c871a2e751ec