--- a/Journal/Paper.thy Tue Mar 04 15:49:36 2014 +0000 +++ b/Journal/Paper.thy Tue Mar 04 16:38:38 2014 +0000 @@ -27,7 +27,7 @@ holdents ("resources") and original_priority ("priority") and DUMMY ("\<^raw:\mbox{$\_\!\_$}>") - + (*>*)