src/HOL/Real/Hyperreal/fuf.ML
changeset 9283 04f1b522cb11
parent 7218 bfa767b4dc51
child 10316 ef2df4ca9da1