# HG changeset patch
# User kleing
# Date 1371856893 25200
# Node ID 3dd63180cdbf51518e110b8550c44c468f48d21f
# Parent  33524382335b736e0737c796d78b6498db260345
Explain to beginners why Complex_Main

diff -r 33524382335b -r 3dd63180cdbf 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