diff -r d7570dbf9f06 -r 6013ca0e6e22 Paper/Paper.thy --- 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