equal
deleted
inserted
replaced
1251 section {* Setups (TBD) *} |
1251 section {* Setups (TBD) *} |
1252 |
1252 |
1253 text {* |
1253 text {* |
1254 In the previous section we used \isacommand{setup} in order to make |
1254 In the previous section we used \isacommand{setup} in order to make |
1255 a theorem attribute known to Isabelle. What happens behind the scenes |
1255 a theorem attribute known to Isabelle. What happens behind the scenes |
1256 is that \isacommand{setup} expects a functions of type |
1256 is that \isacommand{setup} expects a function of type |
1257 @{ML_type "theory -> theory"}: the input theory is the current theory and the |
1257 @{ML_type "theory -> theory"}: the input theory is the current theory and the |
1258 output the theory where the theory attribute has been stored. |
1258 output the theory where the theory attribute has been stored. |
1259 |
1259 |
1260 This is a fundamental principle in Isabelle. A similar situation occurs |
1260 This is a fundamental principle in Isabelle. A similar situation occurs |
1261 for example with declaring constants. The function that declares a |
1261 for example with declaring constants. The function that declares a |
1307 There are theories, proof contexts and local theories (in this order, if you |
1307 There are theories, proof contexts and local theories (in this order, if you |
1308 want to order them). |
1308 want to order them). |
1309 |
1309 |
1310 In contrast to an ordinary theory, which simply consists of a type |
1310 In contrast to an ordinary theory, which simply consists of a type |
1311 signature, as well as tables for constants, axioms and theorems, a local |
1311 signature, as well as tables for constants, axioms and theorems, a local |
1312 theory also contains additional context information, such as locally fixed |
1312 theory contains additional context information, such as locally fixed |
1313 variables and local assumptions that may be used by the package. The type |
1313 variables and local assumptions that may be used by the package. The type |
1314 @{ML_type local_theory} is identical to the type of \emph{proof contexts} |
1314 @{ML_type local_theory} is identical to the type of \emph{proof contexts} |
1315 @{ML_type "Proof.context"}, although not every proof context constitutes a |
1315 @{ML_type "Proof.context"}, although not every proof context constitutes a |
1316 valid local theory. |
1316 valid local theory. |
1317 *} |
1317 *} |