isabelle: src/ZF/IMP/Aexp.thy@d7f8dfaad46d (annotated)

482 3a4e092ba69c Initial revision nipkow parents: diff changeset	1	(* Title: ZF/IMP/Aexp.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	Dummy theory merely recording dependence
3a4e092ba69c Initial revision nipkow parents: diff changeset	7	*)
3a4e092ba69c Initial revision nipkow parents: diff changeset	8
3a4e092ba69c Initial revision nipkow parents: diff changeset	9	Aexp = Univ