Mercurial Mercurial > repos > Old_HOL / annotate
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | file | latest | revisions | annotate | diff | comparison | raw | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
IMP/Equiv.thy
author clasohm
Wed, 02 Nov 1994 11:50:09 +0100
changeset 156 fd1be45b64bf
parent 132 47be9d22a0d6
permissions -rw-r--r--
added IOA to isabelle/HOL
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















Old_HOL