--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/IOA/example/Correctness.thy	Wed Nov 02 11:50:09 1994 +0100
@@ -0,0 +1,15 @@
+Correctness = Solve + Impl + Spec + "Lemmas" +
+
+consts
+
+hom :: "'m impl_state => 'm list"
+
+
+rules
+
+hom_def 
+"hom(s) == rq(rec(s)) @ if(rbit(rec(s)) = sbit(sen(s)),  \
+\                          sq(sen(s)),                   \
+\                          ttl(sq(sen(s))))"
+
+end