HOL,ZF/Makefile: enclosed multiple "use" calls in parentheses. This
ensures that if one dies, all die. BUT NOT Pure/Makefile, where
PolyML.use"POLY" makes the identifier "use" visible.
(* Title: HOL/IOA/example/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)), \
\ sq(sen(s)), \
\ ttl(sq(sen(s))))"
end