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