Mercurial Mercurial > repos > isabelle / comparison
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.
src/ZF/IMP/Equiv.thy
changeset 58871 c399ae4b836f
parent 46822 95f1e700b712
child 60770 240563fbf41d
equal deleted inserted replaced
58870:e2c0d8ef29cb 58871:c399ae4b836f 
     1 (*  Title:      ZF/IMP/Equiv.thy
 
     1 (*  Title:      ZF/IMP/Equiv.thy
 
     2     Author:     Heiko Loetzbeyer and Robert Sandner, TU München
 
     2     Author:     Heiko Loetzbeyer and Robert Sandner, TU München
 
     3 *)
 
     3 *)
 
     4 
     4 
     5 header {* Equivalence *}
 
     5 section {* Equivalence *}
 
     6 
     6 
     7 theory Equiv imports Denotation Com begin
 
     7 theory Equiv imports Denotation Com begin
 
     8 
     8 
     9 lemma aexp_iff [rule_format]:
 
     9 lemma aexp_iff [rule_format]:
 
    10   "[| a \<in> aexp; sigma: loc -> nat |] 
    10   "[| a \<in> aexp; sigma: loc -> nat |]
isabelle