1 header {* 

     1 header {* 

     2  {\em abacus} a kind of register machine

     2  {\em abacus} a kind of register machine

     3 *}

     3 *}

     4 

     4 

     5 theory abacus

     5 theory abacus

     7 begin

     7 begin

     8 

     8 

     9 text {*

     9 text {*

    10   {\em Abacus} instructions:

    10   {\em Abacus} instructions:

    11 *}

    11 *}