author | clasohm |
Mon, 11 Mar 1996 23:59:22 +0100 | |
changeset 1570 | fd1b9c721ac7 |
parent 1376 | 92f83b9d17e1 |
permissions | -rw-r--r-- |
1051 | 1 |
(* Title: HOL/IOA/NTP/Correctness.thy |
2 |
ID: $Id$ |
|
3 |
Author: Tobias Nipkow & Konrad Slind |
|
4 |
Copyright 1994 TU Muenchen |
|
5 |
||
6 |
The main correctness proof: Impl implements Spec |
|
7 |
*) |
|
8 |
||
9 |
Correctness = Solve + Impl + Spec + |
|
10 |
||
1570 | 11 |
constdefs |
1051 | 12 |
|
1570 | 13 |
hom :: 'm impl_state => 'm list |
14 |
"hom(s) == rq(rec(s)) @ (if rbit(rec s) = sbit(sen s) then sq(sen s) |
|
15 |
else ttl(sq(sen s)))" |
|
1051 | 16 |
|
17 |
end |