src/HOL/Library/Extended_Real.thy
changeset 70538 fc9ba6fe367f
parent 70367 81b65ddac59f
child 70532 fcf3b891ccb1
equal deleted inserted replaced
70537:17160e0a60b6 70538:fc9ba6fe367f