src/HOL/Library/Extended_Nonnegative_Real.thy
changeset 69107 c2de7a5c8de9
parent 69064 5840724b1d71
child 69260 0a9688695a1b
equal deleted inserted replaced
69106:742c88258cf8 69107:c2de7a5c8de9