src/HOL/ex/Locales.thy
changeset 12356 ce0961b1f536
parent 12105 1e4451999200
child 12507 cc36d5da9bc0
equal deleted inserted replaced
12355:c8d3c3d09080 12356:ce0961b1f536
    23   mathematical structures (by the inevitable group theory example).
    23   mathematical structures (by the inevitable group theory example).
    24 *}
    24 *}
    25 
    25 
    26 text_raw {*
    26 text_raw {*
    27   \newcommand{\isasyminv}{\isasyminverse}
    27   \newcommand{\isasyminv}{\isasyminverse}
    28   \newcommand{\isasymone}{\isamath{1}}
       
    29   \newcommand{\isasymIN}{\isatext{\isakeyword{in}}}
    28   \newcommand{\isasymIN}{\isatext{\isakeyword{in}}}
    30 *}
    29 *}
    31 
    30 
    32 
    31 
    33 subsection {* Local contexts as mathematical structures *}
    32 subsection {* Local contexts as mathematical structures *}