src/HOL/Library/Extended_Nonnegative_Real.thy
changeset 74154 62b0577123a5
parent 73933 fa92bc604c59
child 74325 8d0c2d74ad63
equal deleted inserted replaced
74153:46f66e821f5c 74154:62b0577123a5