PrioG.thy
changeset 89 2056d9f481e2
parent 88 83dd5345d5d0
child 90 ed938e2246b9
equal deleted inserted replaced
88:83dd5345d5d0 89:2056d9f481e2
     1 <<<<<<< local
     1 theory PrioG
     2 theory Correctness
     2 imports CpsG
     3 imports PIPBasics
       
     4 begin
     3 begin
     5 
     4 
     6 
     5 
     7 text {* 
     6 text {* 
     8   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}.
  1608 qed
  1607 qed
  1609 
  1608 
  1610 
  1609 
  1611 end
  1610 end
  1612 end
  1611 end
  1613 >>>>>>> other