src/HOL/Hyperreal/HLog.thy
changeset 15827 5fdf2d8dab9c
parent 15140 322485b816ac
child 17298 ad73fb6144cf
equal deleted inserted replaced
15826:e9b4c9feb296 15827:5fdf2d8dab9c