src/HOL/Hyperreal/transfer.ML
changeset 22898 38ae2815989f
parent 22846 fb79144af9a3
child 24039 273698405054