src/HOL/Real/Real.thy
changeset 19640 40ec89317425
parent 19023 5652a536b7e8
child 20505 1e223f64bd59
equal deleted inserted replaced
19639:d9079a9ccbfb 19640:40ec89317425
       
     1 
       
     2 (* $Id$ *)
       
     3 
     1 theory Real
     4 theory Real
     2 imports ContNotDenum RealPow
     5 imports ContNotDenum Ferrante_Rackoff
     3 begin
     6 begin
     4 end
     7 end