pointer to the other proof direction

--- a/src/HOL/IMP/Compiler2.thy	Wed Mar 19 20:50:24 2014 -0700
+++ b/src/HOL/IMP/Compiler2.thy	Thu Mar 20 09:47:43 2014 +0100
@@ -4,6 +4,11 @@
 imports Compiler
 begin
 
+text {*
+The preservation of the source code semantics is already shown in the 
+parent theory @{theory Compiler}. This here shows the second direction.
+*}
+
 section {* Compiler Correctness, Reverse Direction *}
 
 subsection {* Definitions *}