Mercurial Mercurial > hg > pip / 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.
Correctness.thy
changeset 69 1dc801552dfd
parent 68 db196b066b97
child 73 b0054fb0d1ce
equal deleted inserted replaced
68:db196b066b97 69:1dc801552dfd 
     1 theory Correctness
 
     1 theory Correctness
 
     2 imports PIPBasics
 
     2 imports PIPBasics
 
     3 begin
 
     3 begin
 
       
     4 
     4 
     5 
     5 text {* 
     6 text {* 
     6   The following two auxiliary lemmas are used to reason about @{term Max}.
 
     7   The following two auxiliary lemmas are used to reason about @{term Max}.
 
     7 *}
 
     8 *}
 
     8 lemma image_Max_eqI: 
     9 lemma image_Max_eqI:
pip