isabelle: src/ZF/IMP/Evalb0.thy@c5a7a7685826 (annotated)

482 3a4e092ba69c Initial revision nipkow parents: diff changeset	1	(* Title: ZF/IMP/Evalb0.thy
3a4e092ba69c Initial revision nipkow parents: diff changeset	2	ID: $Id$
3a4e092ba69c Initial revision nipkow parents: diff changeset	3	Author: Heiko Loetzbeyer & Robert Sandner, TUM
3a4e092ba69c Initial revision nipkow parents: diff changeset	4	Copyright 1994 TUM
3a4e092ba69c Initial revision nipkow parents: diff changeset	5	*)
3a4e092ba69c Initial revision nipkow parents: diff changeset	6
3a4e092ba69c Initial revision nipkow parents: diff changeset	7	Evalb0 = Evala + Bexp +
3a4e092ba69c Initial revision nipkow parents: diff changeset	8
3a4e092ba69c Initial revision nipkow parents: diff changeset	9	consts
3a4e092ba69c Initial revision nipkow parents: diff changeset	10	evalb :: "i"
3a4e092ba69c Initial revision nipkow parents: diff changeset	11	"@evalb" :: "[i,i,i] => o" ("<_,_>/ -b-> _")
3a4e092ba69c Initial revision nipkow parents: diff changeset	12
3a4e092ba69c Initial revision nipkow parents: diff changeset	13	translations
3a4e092ba69c Initial revision nipkow parents: diff changeset	14	"<be,sig> -b-> b" == "<be,sig,b> : evalb"
3a4e092ba69c Initial revision nipkow parents: diff changeset	15	end