author | clasohm |
Fri, 01 Dec 1995 12:03:13 +0100 | |
changeset 1376 | 92f83b9d17e1 |
parent 1151 | c820b3cc3df0 |
child 1570 | fd1b9c721ac7 |
permissions | -rw-r--r-- |
(* Title: HOL/IOA/NTP/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 defs hom_def "hom(s) == rq(rec(s)) @ (if rbit(rec s) = sbit(sen s) then sq(sen s) else ttl(sq(sen s)))" end