src/HOL/Library/Extended_Real.thy
changeset 65380 ae93953746fc
parent 64272 f76b6dda2e56
child 65680 378a2f11bec9
equal deleted inserted replaced
65379:76a96e32bd23 65380:ae93953746fc