src/HOL/Library/Extended_Real.thy
changeset 58187 d2ddd401d74d
parent 58042 ffa9e39763e3
child 58249 180f1b3508ed