src/HOL/Hyperreal/NatStar.ML
changeset 13419 902ec83c1ca9
parent 12486 0ed8bdd883e0
child 13810 c3fbfd472365
equal deleted inserted replaced
13418:7c0ba9dba978 13419:902ec83c1ca9