isabelle: src/ZF/IMP/Bexp.thy@3a4e092ba69c (annotated)

482 3a4e092ba69c Initial revision nipkow parents: diff changeset	1	(* Title: ZF/IMP/Bexp.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	Bexp = Aexp