src/HOL/IMP/Types.thy

--- a/src/HOL/IMP/Types.thy	Fri Jun 21 16:20:47 2013 +0200
+++ b/src/HOL/IMP/Types.thy	Fri Jun 21 16:21:33 2013 -0700
@@ -2,6 +2,9 @@
 
 theory Types imports Star Complex_Main begin
 
+text {* We build on @{theory Complex_Main} instead of @{theory Main} to access
+the real numbers. *}
+
 subsection "Arithmetic Expressions"
 
 datatype val = Iv int | Rv real