src/HOL/Hyperreal/fuf.ML
changeset 14322 fa78e7eb1dac
parent 14299 0b5c0b0a3eba
child 17298 ad73fb6144cf
equal deleted inserted replaced
14321:55c688d2eefa 14322:fa78e7eb1dac