src/HOL/Analysis/Continuous_Extension.thy
changeset 64492 98215fa4f8d1
parent 64267 b9a1486e79be
child 66289 2562f151541c
equal deleted inserted replaced
64491:6a1a1bbfcb93 64492:98215fa4f8d1