Journal/Paper.thy
changeset 28 7fa738a9615a
parent 27 6b1141c5e24c
child 32 e861aff29655
equal deleted inserted replaced
27:6b1141c5e24c 28:7fa738a9615a
    25   dependents ("dependants") and
    25   dependents ("dependants") and
    26   cp ("cprec") and
    26   cp ("cprec") and
    27   holdents ("resources") and
    27   holdents ("resources") and
    28   original_priority ("priority") and
    28   original_priority ("priority") and
    29   DUMMY  ("\<^raw:\mbox{$\_\!\_$}>")
    29   DUMMY  ("\<^raw:\mbox{$\_\!\_$}>")
    30 
    30  
    31   
    31   
    32 (*>*)
    32 (*>*)
    33 
    33 
    34 section {* Introduction *}
    34 section {* Introduction *}
    35 
    35