src/HOL/Analysis/Continuous_Extension.thy
changeset 72644 0e422e806ef3
parent 71255 4258ee13f5d4
child 76987 4c275405faae
equal deleted inserted replaced
72641:4eea17b3ac58 72644:0e422e806ef3