src/HOL/Library/Extended_Real.thy
changeset 77490 2c86ea8961b5
parent 74325 8d0c2d74ad63
child 81332 f94b30fa2b6c
equal deleted inserted replaced
77435:df1150ec6cd7 77490:2c86ea8961b5