src/HOLCF/IOA/NTP/Correctness.thy

added find_theorems.ML, ../simplifier.ML;

(*  Title:      HOL/IOA/NTP/Correctness.thy
    ID:         $Id$
    Author:     Tobias Nipkow & Konrad Slind

The main correctness proof: Impl implements Spec.
*)

Correctness = Impl + Spec +

constdefs

  hom :: 'm impl_state => 'm list
  "hom(s) == rq(rec(s)) @ (if rbit(rec s) = sbit(sen s) then sq(sen s) 
                           else tl(sq(sen s)))"

end