2 section {*

     1 section {*

     3   This file contains lemmas used to guide the recalculation of current precedence 

     2   This file contains lemmas used to guide the recalculation of current precedence 

     4   after every system call (or system operation)

     3   after every system call (or system operation)

     5 *}

     4 *}

     6 theory ExtGG

     5 theory ExtGG

  1626 qed

  1625 qed

  1627 

  1626 

  1628 end

  1627 end

  1629 end

  1628 end

  1630 

  1629