changeset 482 | 3a4e092ba69c |
--- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/ZF/IMP/Evalc0.thy Thu Jul 21 14:27:00 1994 +0200 @@ -0,0 +1,15 @@ +(* Title: ZF/IMP/Evalc0.thy + ID: $Id$ + Author: Heiko Loetzbeyer & Robert Sandner, TUM + Copyright 1994 TUM +*) + +Evalc0 = Evalb + Com + Assign + + +consts + evalc :: "i" + "@evalc" :: "[i,i,i] => o" ("<_,_>/ -c-> _") + +translations + "<ce,sig> -c-> s" == "<ce,sig,s> : evalc" +end