src/HOL/Library/Extended_Real.thy
changeset 63745 dde79b7faddf
parent 63680 6e1e8b5abbfa
child 63882 018998c00003