src/HOL/Hyperreal/SEQ.thy
changeset 11405 b6e3ac38397d
parent 10751 a81ea5d3dd41
child 11701 3d51fbf81c17