equal
deleted
inserted
replaced
1321 section {* Conversions\label{sec:conversion} *} |
1321 section {* Conversions\label{sec:conversion} *} |
1322 |
1322 |
1323 text {* |
1323 text {* |
1324 |
1324 |
1325 Conversions are a thin layer on top of Isabelle's inference kernel, and |
1325 Conversions are a thin layer on top of Isabelle's inference kernel, and |
1326 can be viewed be as a controllable, bare-bone version of Isabelle's simplifier. |
1326 can be viewed as a controllable, bare-bone version of Isabelle's simplifier. |
1327 One difference between conversions and the simplifier is that the former |
1327 One difference between conversions and the simplifier is that the former |
1328 act on @{ML_type cterm}s while the latter acts on @{ML_type thm}s. |
1328 act on @{ML_type cterm}s while the latter acts on @{ML_type thm}s. |
1329 However, we will also show in this section how conversions can be applied |
1329 However, we will also show in this section how conversions can be applied |
1330 to theorems via tactics. The type for conversions is |
1330 to theorems via tactics. The type for conversions is |
1331 *} |
1331 *} |