replaced Sorts.DOMAIN by general Sorts.CLASS_ERROR;
add_types etc.: reject qualified dummy types -- prevents users from messing up some internal conventions;
(* Title: HOL/IOA/NTP/Correctness.thy
ID: $Id$
Author: Tobias Nipkow & Konrad Slind
*)
header {* The main correctness proof: Impl implements Spec *}
theory Correctness
imports Impl Spec
begin
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)))"
ML {* use_legacy_bindings (the_context ()) *}
end