1363 ML{*Attrib.setup @{binding "my_sym"} (Scan.succeed my_symmetric)

  1363 ML{*Attrib.setup @{binding "my_sym"} (Scan.succeed my_symmetric)

  1364   "applying the sym rule" *}

  1364   "applying the sym rule" *}

  1365 

  1365 

  1366 text {*

  1366 text {*

  1367   This gives a function from @{ML_type "theory -> theory"}, which

  1367   This gives a function from @{ML_type "theory -> theory"}, which

  1369 

  1370 

  1370   As an example of a slightly more complicated theorem attribute, we implement 

  1371   As an example of a slightly more complicated theorem attribute, we implement 

  1371   our own version of @{text "[THEN \<dots>]"}. This attribute will take a list of theorems

  1372   our own version of @{text "[THEN \<dots>]"}. This attribute will take a list of theorems

  1372   as argument and resolve the theorem with this list (one theorem 

  1373   as argument and resolve the theorem with this list (one theorem 

  1373   after another). The code for this attribute is

  1374   after another). The code for this attribute is

  1543   theory contains additional context information, such as locally fixed

  1544   theory contains additional context information, such as locally fixed

  1544   variables and local assumptions that may be used by the package. The type

  1545   variables and local assumptions that may be used by the package. The type

  1545   @{ML_type local_theory} is identical to the type of \emph{proof contexts}

  1546   @{ML_type local_theory} is identical to the type of \emph{proof contexts}

  1546   @{ML_type "Proof.context"}, although not every proof context constitutes a

  1547   @{ML_type "Proof.context"}, although not every proof context constitutes a

  1547   valid local theory.

  1548   valid local theory.

  1548 *}

  1551 *}

  1549 

  1552 

  1550 section {* Setups (TBD) *}

  1553 section {* Setups (TBD) *}

  1551 

  1554 

  1552 text {*

  1555 text {*

  1553   In the previous section we used \isacommand{setup} in order to make

  1558   In the previous section we used \isacommand{setup} in order to make

  1554   a theorem attribute known to Isabelle. What happens behind the scenes

  1559   a theorem attribute known to Isabelle. What happens behind the scenes

  1555   is that \isacommand{setup} expects a function of type 

  1560   is that \isacommand{setup} expects a function of type 

  1556   @{ML_type "theory -> theory"}: the input theory is the current theory and the 

  1561   @{ML_type "theory -> theory"}: the input theory is the current theory and the 

  1557   output the theory where the theory attribute has been stored.

  1562   output the theory where the theory attribute has been stored.