equal
deleted
inserted
replaced
1312 |
1312 |
1313 (FIXME: We did not do anything with morphisms. Anything interesting |
1313 (FIXME: We did not do anything with morphisms. Anything interesting |
1314 one can say about them?) |
1314 one can say about them?) |
1315 *} |
1315 *} |
1316 |
1316 |
1317 section {* Conversions *} |
1317 section {* Conversions\label{sec:conversion} *} |
1318 |
1318 |
1319 text {* |
1319 text {* |
1320 conversions: core of the simplifier |
1320 conversions: core of the simplifier |
1321 |
1321 |
1322 see: Pure/conv.ML |
1322 see: Pure/conv.ML |