src/HOL/Hyperreal/Poly.ML
changeset 13585 db4005b40cc6
parent 12481 ea5d6da573c5
child 13601 fd3e3d6b37b2