author | nipkow |
Wed, 31 Aug 1994 16:25:19 +0200 | |
changeset 132 | 47be9d22a0d6 |
parent 131 | 41bf53133ba6 |
permissions | -rw-r--r-- |
132 | 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 |