src/HOL/Library/Extended_Real.thy
changeset 59370 b13ff987c559
parent 59115 f65ac77f7e07
child 59425 c5e79df8cc21
equal deleted inserted replaced
59369:7090199d3f78 59370:b13ff987c559