src/HOL/Analysis/Regularity.thy
changeset 66524 0d8dab1f6903
parent 64267 b9a1486e79be
child 68046 6aba668aea78
equal deleted inserted replaced
66523:5a1a2ac950c2 66524:0d8dab1f6903