src/HOL/Real/Hyperreal/HSeries.ML
changeset 10754 9bc30e51144c
parent 10712 351ba950d4d9
equal deleted inserted replaced
10753:e43e017df8c1 10754:9bc30e51144c