# HG changeset patch
# User kleing
# Date 1395305263 -3600
# Node ID 18378a709991b1e33781a04fc32752805e88c789
# Parent  7696903b9e61efd2b8630a77dd4e716e48fc0a0a
pointer to the other proof direction

diff -r 7696903b9e61 -r 18378a709991 src/HOL/IMP/Compiler2.thy
--- 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 *}