src/HOL/Real/Real.thy
author wenzelm
Tue May 16 13:01:22 2006 +0200 (2006-05-16)
changeset 19640 40ec89317425
parent 19023 5652a536b7e8
child 20505 1e223f64bd59
permissions -rw-r--r--
added Ferrante and Rackoff Algorithm -- by Amine Chaieb;
wenzelm@19640
     1
wenzelm@19640
     2
(* $Id$ *)
wenzelm@19640
     3
nipkow@15536
     4
theory Real
wenzelm@19640
     5
imports ContNotDenum Ferrante_Rackoff
nipkow@15536
     6
begin
wenzelm@19640
     7
end