equal
deleted
inserted
replaced
51 *} |
51 *} |
52 |
52 |
53 |
53 |
54 text {* |
54 text {* |
55 \begin{readmore} |
55 \begin{readmore} |
56 XXX |
56 For more information see @{ML_file "Pure/Tools/named_thms.ML"}. |
57 |
|
58 \end{readmore} |
57 \end{readmore} |
59 *} |
58 *} |
60 |
59 |
61 |
60 |
62 end |
61 end |