src/HOL/Analysis/Regularity.thy
changeset 78778 d495e71707d4
parent 74362 0135a0c77b64
equal deleted inserted replaced
78777:3b424f9cd5eb 78778:d495e71707d4