src/HOL/Tools/Argo/argo_real.ML
changeset 70901 94a0c47b8553
parent 67149 e61557884799
child 74282 c2ee8d993d6a
equal deleted inserted replaced
70900:954e7f79c25a 70901:94a0c47b8553