--- a/src/HOL/IMP/Compiler2.thy Fri Aug 17 11:26:35 2018 +0000
+++ b/src/HOL/IMP/Compiler2.thy Mon Aug 20 20:54:26 2018 +0200
@@ -1,16 +1,16 @@
(* Author: Gerwin Klein *)
+section \<open>Compiler Correctness, Reverse Direction\<close>
+
theory Compiler2
imports Compiler
begin
text \<open>
The preservation of the source code semantics is already shown in the
-parent theory @{theory "HOL-IMP.Compiler"}. This here shows the second direction.
+parent theory @{text "Compiler"}. This here shows the second direction.
\<close>
-section \<open>Compiler Correctness, Reverse Direction\<close>
-
subsection \<open>Definitions\<close>
text \<open>Execution in @{term n} steps for simpler induction\<close>