13 abbreviation

    13 abbreviation

    14   "update2 p a \<equiv> update a p"

    14   "update2 p a \<equiv> update a p"

    15 

    15 

    16 consts DUMMY::'a

    16 consts DUMMY::'a

    17 

    17 

    20 notation (Rule output)

    19 notation (Rule output)

    21   "==>"  ("\<^raw:\mbox{}\inferrule{\mbox{>_\<^raw:}}>\<^raw:{\mbox{>_\<^raw:}}>")

    20   "==>"  ("\<^raw:\mbox{}\inferrule{\mbox{>_\<^raw:}}>\<^raw:{\mbox{>_\<^raw:}}>")

    22 

    21 

    23 syntax (Rule output)

    22 syntax (Rule output)

    24   "_bigimpl" :: "asms \<Rightarrow> prop \<Rightarrow> prop"

    23   "_bigimpl" :: "asms \<Rightarrow> prop \<Rightarrow> prop"

    57   set ("") and

    56   set ("") and

    58   W0 ("W\<^bsub>\<^raw:\hspace{-2pt}>Bk\<^esub>") and

    57   W0 ("W\<^bsub>\<^raw:\hspace{-2pt}>Bk\<^esub>") and

    59   W1 ("W\<^bsub>\<^raw:\hspace{-2pt}>Oc\<^esub>") and

    58   W1 ("W\<^bsub>\<^raw:\hspace{-2pt}>Oc\<^esub>") and

    60   update2 ("update") and

    59   update2 ("update") and

    61   tm_wf0 ("wf") and

    60   tm_wf0 ("wf") and

    63   tcopy_begin ("cbegin") and

    61   tcopy_begin ("cbegin") and

    64   tcopy_loop ("cloop") and

    62   tcopy_loop ("cloop") and

    65   tcopy_end ("cend") and

    63   tcopy_end ("cend") and

    66   step0 ("step") and

    64   step0 ("step") and

    67   tcontra ("contra") and

    65   tcontra ("contra") and