src/HOL/Hyperreal/HyperPow.ML
changeset 14303 995212a00a50
parent 14299 0b5c0b0a3eba
child 14305 f17ca9f6dc8c
equal deleted inserted replaced
14302:6c24235e8d5d 14303:995212a00a50