isabelle: src/ZF/IMP/Evala0.thy@8b9845807f77 (annotated)

482 3a4e092ba69c Initial revision nipkow parents: diff changeset	1	(* Title: ZF/IMP/Evala0.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	Evala0 = Aexp +
3a4e092ba69c Initial revision nipkow parents: diff changeset	8
3a4e092ba69c Initial revision nipkow parents: diff changeset	9	consts evala :: "i"
3a4e092ba69c Initial revision nipkow parents: diff changeset	10	"@evala" :: "[i,i,i] => o" ("<_,_>/ -a-> _")
3a4e092ba69c Initial revision nipkow parents: diff changeset	11
3a4e092ba69c Initial revision nipkow parents: diff changeset	12	translations
3a4e092ba69c Initial revision nipkow parents: diff changeset	13	"<ae,sig> -a-> n" == "<ae,sig,n> : evala"
3a4e092ba69c Initial revision nipkow parents: diff changeset	14	end