doc-src/IsarImplementation/Thy/prelim.thy
changeset 20205 7b2958d3d575
parent 18554 bff7a1466fe4
child 20214 525f934b438b
equal deleted inserted replaced
20204:2842450d0eee 20205:7b2958d3d575
    45 
    45 
    46 \item or a control symbol ``\verb,\,\verb,<^,@{text
    46 \item or a control symbol ``\verb,\,\verb,<^,@{text
    47 "ident"}\verb,>,'', for example ``\verb,\,\verb,<^bold>,'',
    47 "ident"}\verb,>,'', for example ``\verb,\,\verb,<^bold>,'',
    48 
    48 
    49 \item or a raw control symbol ``\verb,\,\verb,<^raw:,@{text
    49 \item or a raw control symbol ``\verb,\,\verb,<^raw:,@{text
    50 "\<dots>"}\verb,>,'' where ``@{text "\<dots>"}'' refers to any printable ASCII
    50 "\<dots>"}\verb,>,'' where ``@{text "\<dots>"}'' refers to any
    51 character (excluding ``\verb,>,'') or non-ASCII character, for example
    51 printable ASCII character (excluding ``\verb,.,'' and ``\verb,>,'') or
    52 ``\verb,\,\verb,<^raw:$\sum_{i = 1}^n$>,'',
    52 non-ASCII character, for example ``\verb,\,\verb,<^raw:$\sum_{i =
       
    53 1}^n$>,'',
    53 
    54 
    54 \item or a numbered raw control symbol ``\verb,\,\verb,<^raw,@{text
    55 \item or a numbered raw control symbol ``\verb,\,\verb,<^raw,@{text
    55 "nnn"}\verb,>, where @{text "nnn"} are digits, for example
    56 "nnn"}\verb,>, where @{text "nnn"} are digits, for example
    56 ``\verb,\,\verb,<^raw42>,''.
    57 ``\verb,\,\verb,<^raw42>,''.
    57 
    58