--- a/Paper/Paper.thy	Tue Feb 12 13:37:07 2013 +0000
+++ b/Paper/Paper.thy	Wed Feb 13 20:08:14 2013 +0000
@@ -15,8 +15,7 @@
 
 consts DUMMY::'a
 
-
-(* THEOREMS *)
+(* Theorems as inference rules from LaTeXsugar.thy *)
 notation (Rule output)
   "==>"  ("\<^raw:\mbox{}\inferrule{\mbox{>_\<^raw:}}>\<^raw:{\mbox{>_\<^raw:}}>")
 
@@ -59,7 +58,6 @@
   W1 ("W\<^bsub>\<^raw:\hspace{-2pt}>Oc\<^esub>") and
   update2 ("update") and
   tm_wf0 ("wf") and
-  (*is_even ("iseven") and*)
   tcopy_begin ("cbegin") and
   tcopy_loop ("cloop") and
   tcopy_end ("cend") and