IMP/Equiv.thy
author wenzelm
Wed, 21 Sep 1994 15:40:41 +0200
changeset 145 a9f7ff3a464c
parent 132 47be9d22a0d6
permissions -rw-r--r--
minor cleanup, added 'axclass', 'instance', 'syntax', 'defs' sections;
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
132
47be9d22a0d6 Renamed a few types and vars
nipkow
parents: 131
diff changeset
     1
(*  Title: 	HOL/IMP/Equiv.thy
131
41bf53133ba6 Equivalence of op. and den. sem. for simple while language.
nipkow
parents:
diff changeset
     2
    ID:         $Id$
41bf53133ba6 Equivalence of op. and den. sem. for simple while language.
nipkow
parents:
diff changeset
     3
    Author: 	Heiko Loetzbeyer & Robert Sandner, TUM
41bf53133ba6 Equivalence of op. and den. sem. for simple while language.
nipkow
parents:
diff changeset
     4
    Copyright   1994 TUM
41bf53133ba6 Equivalence of op. and den. sem. for simple while language.
nipkow
parents:
diff changeset
     5
*)
41bf53133ba6 Equivalence of op. and den. sem. for simple while language.
nipkow
parents:
diff changeset
     6
41bf53133ba6 Equivalence of op. and den. sem. for simple while language.
nipkow
parents:
diff changeset
     7
Equiv = Denotation