src/HOL/RealDef.thy
changeset 35043 07dbdf60d5ad
parent 35032 7efe662e41b4
child 35050 9f841f20dca6
equal deleted inserted replaced
35042:a27b48967b26 35043:07dbdf60d5ad