src/HOL/Hyperreal/Poly.ML
changeset 12597 14822e4436bf
parent 12481 ea5d6da573c5
child 13601 fd3e3d6b37b2