src/HOL/Real/Hyperreal/fuf.ML
changeset 7965 a00ad4ca6232
parent 7218 bfa767b4dc51
child 10316 ef2df4ca9da1