src/HOL/ex/Locales.thy
changeset 12965 c8a97eb1e3c7
parent 12955 f4d60f358cb6
child 13107 8743cc847224
equal deleted inserted replaced
12964:2ac9265b2cd5 12965:c8a97eb1e3c7
     9 theory Locales = Main:
     9 theory Locales = Main:
    10 
    10 
    11 text_raw {*
    11 text_raw {*
    12   \newcommand{\isasyminv}{\isasyminverse}
    12   \newcommand{\isasyminv}{\isasyminverse}
    13   \newcommand{\isasymIN}{\isatext{\isakeyword{in}}}
    13   \newcommand{\isasymIN}{\isatext{\isakeyword{in}}}
    14   \newcommand{\isasymUSES}{\isatext{\isakeyword{uses}}}
    14   \newcommand{\isasymINCLUDES}{\isatext{\isakeyword{includes}}}
    15 *}
    15 *}
    16 
    16 
    17 subsection {* Overview *}
    17 subsection {* Overview *}
    18 
    18 
    19 text {*
    19 text {*
   197 text {*
   197 text {*
   198   We see that the initial import of @{text group} within the
   198   We see that the initial import of @{text group} within the
   199   definition of @{text abelian_group} is actually evaluated
   199   definition of @{text abelian_group} is actually evaluated
   200   dynamically.  Thus any results in @{text group} are made available
   200   dynamically.  Thus any results in @{text group} are made available
   201   to the derived context of @{text abelian_group} as well.  Note that
   201   to the derived context of @{text abelian_group} as well.  Note that
   202   the alternative context element @{text \<USES>} would import
   202   the alternative context element @{text \<INCLUDES>} would import
   203   existing locales in a static fashion, without participating in
   203   existing locales in a static fashion, without participating in
   204   further facts emerging later on.
   204   further facts emerging later on.
   205 
   205 
   206   \medskip Some more properties of inversion in general group theory
   206   \medskip Some more properties of inversion in general group theory
   207   follow.
   207   follow.