src/HOL/Analysis/Continuous_Extension.thy
changeset 80177 1478555580af
parent 78277 6726b20289b4
equal deleted inserted replaced
80176:7fefa7839ac6 80177:1478555580af