isabelle: src/ZF/IMP/Evalc0.thy@2937a854e3d7 (annotated)

482 3a4e092ba69c Initial revision nipkow parents: diff changeset	1	(* Title: ZF/IMP/Evalc0.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	Evalc0 = Evalb + Com + Assign +
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	evalc :: "i"
3a4e092ba69c Initial revision nipkow parents: diff changeset	11	"@evalc" :: "[i,i,i] => o" ("<_,_>/ -c-> _")
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	"<ce,sig> -c-> s" == "<ce,sig,s> : evalc"
3a4e092ba69c Initial revision nipkow parents: diff changeset	15	end