doc-src/IsarAdvanced/Codegen/codegen.tex
changeset 24348 c708ea5b109a
parent 22798 e3962371f568
child 25870 a6a21adf3b55
equal deleted inserted replaced
24347:245ff8661b8c 24348:c708ea5b109a
    30 \newcommand{\isasymFIX}{\cmd{fix}}
    30 \newcommand{\isasymFIX}{\cmd{fix}}
    31 \newcommand{\isasymASSUME}{\cmd{assume}}
    31 \newcommand{\isasymASSUME}{\cmd{assume}}
    32 \newcommand{\isasymSHOW}{\cmd{show}}
    32 \newcommand{\isasymSHOW}{\cmd{show}}
    33 \newcommand{\isasymNOTE}{\cmd{note}}
    33 \newcommand{\isasymNOTE}{\cmd{note}}
    34 \newcommand{\isasymIN}{\cmd{in}}
    34 \newcommand{\isasymIN}{\cmd{in}}
    35 \newcommand{\isasymCODEGEN}{\cmd{code\_gen}}
    35 \newcommand{\isasymEXPORTCODE}{\cmd{export\_code}}
    36 \newcommand{\isasymCODEDATATYPE}{\cmd{code\_datatype}}
    36 \newcommand{\isasymCODEDATATYPE}{\cmd{code\_datatype}}
    37 \newcommand{\isasymCODECONST}{\cmd{code\_const}}
    37 \newcommand{\isasymCODECONST}{\cmd{code\_const}}
    38 \newcommand{\isasymCODETYPE}{\cmd{code\_type}}
    38 \newcommand{\isasymCODETYPE}{\cmd{code\_type}}
    39 \newcommand{\isasymCODECLASS}{\cmd{code\_class}}
    39 \newcommand{\isasymCODECLASS}{\cmd{code\_class}}
    40 \newcommand{\isasymCODEINSTANCE}{\cmd{code\_instance}}
    40 \newcommand{\isasymCODEINSTANCE}{\cmd{code\_instance}}