diff -r 37a6e2f55230 -r 44ff2275d44f IOA/example/Correctness.thy
--- a/IOA/example/Correctness.thy	Wed Nov 09 19:50:36 1994 +0100
+++ b/IOA/example/Correctness.thy	Wed Nov 09 19:51:09 1994 +0100
@@ -1,11 +1,18 @@
-Correctness = Solve + Impl + Spec + "Lemmas" +
+(*  Title:      HOL/IOA/example/Correctness.thy
+    ID:         $Id$
+    Author:     Tobias Nipkow & Konrad Slind
+    Copyright   1994  TU Muenchen
+
+The main correctness proof: Impl implements Spec
+*)
+
+Correctness = Solve + Impl + Spec +
 
 consts
 
 hom :: "'m impl_state => 'm list"
 
-
-rules
+defs
 
 hom_def 
 "hom(s) == rq(rec(s)) @ if(rbit(rec(s)) = sbit(sen(s)),  \