src/HOL/Hyperreal/hypreal_arith.ML
changeset 23590 ad95084a5c63
parent 20254 58b71535ed00
child 24075 366d4d234814