src/HOL/Real.thy

--- a/src/HOL/Real.thy	Thu Sep 29 18:52:34 2016 +0200
+++ b/src/HOL/Real.thy	Thu Sep 29 20:54:44 2016 +0200
@@ -10,7 +10,7 @@
 section \<open>Development of the Reals using Cauchy Sequences\<close>
 
 theory Real
-imports Rat
+imports Rat Argo
 begin
 
 text \<open>
@@ -1807,4 +1807,9 @@
   for x y :: real
   by auto
 
+
+subsection \<open>Setup for Argo\<close>
+
+ML_file "Tools/Argo/argo_real.ML"
+
 end