# HG changeset patch
# User nipkow
# Date 1352900714 -3600
# Node ID 7110422d4cb3f80ef8224d7d32f703d26c50d017
# Parent  43753eca324a31af9a371dd8475dff8efec87e67
tuned text

diff -r 43753eca324a -r 7110422d4cb3 src/HOL/IMP/Comp_Rev.thy
--- a/src/HOL/IMP/Comp_Rev.thy	Wed Nov 14 14:11:47 2012 +0100
+++ b/src/HOL/IMP/Comp_Rev.thy	Wed Nov 14 14:45:14 2012 +0100
@@ -2,7 +2,7 @@
 imports Compiler
 begin
 
-section {* Compiler Correctness, 2nd direction *}
+section {* Compiler Correctness, Reverse Direction *}
 
 subsection {* Definitions *}
 
diff -r 43753eca324a -r 7110422d4cb3 src/HOL/IMP/Compiler.thy
--- a/src/HOL/IMP/Compiler.thy	Wed Nov 14 14:11:47 2012 +0100
+++ b/src/HOL/IMP/Compiler.thy	Wed Nov 14 14:45:14 2012 +0100
@@ -1,6 +1,6 @@
 (* Author: Tobias Nipkow *)
 
-header "A Compiler for IMP"
+header "Compiler for IMP"
 
 theory Compiler imports Big_Step 
 begin