Mercurial Mercurial > repos > isabelle / changeset
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | raw | gz | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
tuned text
authornipkow
Wed, 14 Nov 2012 14:45:14 +0100
changeset 50061 7110422d4cb3
parent 50060 43753eca324a
child 50062 e038198f7d08
tuned text
src/HOL/IMP/Comp_Rev.thy file | annotate | diff | comparison | revisions
src/HOL/IMP/Compiler.thy file | annotate | diff | comparison | revisions 
--- 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 *}
 
--- 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
isabelle