39   @{ML_text foo}:

    39   @{ML_text foo}:

    40 *}

    40 *}

    41 

    41 

    42 lemma rule1[foo]: "A" sorry

    42 lemma rule1[foo]: "A" sorry

    43 lemma rule2[foo]: "B" sorry

    43 lemma rule2[foo]: "B" sorry

    44 

    45 

    45 text {* undeclare them: *}

    46 text {* undeclare them: *}

    46 

    47 

    47 declare rule1[foo del]

    48 declare rule1[foo del]

    48 

    49 

    52 

    53 

    53 text {* 

    54 text {* 

    54   In an ML-context the rules marked with @{ML_text "foo"} an be retrieved

    55   In an ML-context the rules marked with @{ML_text "foo"} an be retrieved

    55   using

    56   using

    56 

    57 

    58 

    59 

    59   \begin{readmore}

    60   \begin{readmore}

    60   For more information see @{ML_file "Pure/Tools/named_thms.ML"}.

    61   For more information see @{ML_file "Pure/Tools/named_thms.ML"}.

    61   \end{readmore}

    62   \end{readmore}

    62  *}

    63  *}