src/HOL/IMP/Compiler.thy

--- a/src/HOL/IMP/Compiler.thy	Thu Oct 26 14:52:41 2000 +0200
+++ b/src/HOL/IMP/Compiler.thy	Thu Oct 26 14:59:38 2000 +0200
@@ -1,3 +1,11 @@
+(*  Title:      HOL/IMP/Compiler.thy
+    ID:         $Id$
+    Author:     Tobias Nipkow, TUM
+    Copyright   1996 TUM
+
+A simple compiler for a simplistic machine.
+*)
+
 theory Compiler = Natural:
 
 datatype instr = ASIN loc aexp | JMPF bexp nat | JMPB nat