src/HOL/Real.thy
changeset 28952 15a4b2cf8c34
parent 27964 1e0303048c0b
child 29026 5fbaa05f637f
equal deleted inserted replaced
28948:1860f016886d 28952:15a4b2cf8c34
       
     1 theory Real
       
     2 imports ContNotDenum "~~/src/HOL/Real/RealVector"
       
     3 begin
       
     4 
       
     5 end