--- 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)), \