src/HOL/Hyperreal/Filter.ML
changeset 15004 44ac09ba7213
parent 13551 b7f64ee8da84
equal deleted inserted replaced
15003:6145dd7538d7 15004:44ac09ba7213