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 |
1368 can be used for example with \isacommand{setup} or with |
1368 can be used for example with \isacommand{setup} or with |
1369 @{ML "Context.>> o Context.map_theory"}. |
1369 @{ML "Context.>> o Context.map_theory"}.\footnote{\bf FIXME: explain what happens here.} |
1370 |
1370 |
1371 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 |
1372 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 |
1373 as argument and resolve the theorem with this list (one theorem |
1373 as argument and resolve the theorem with this list (one theorem |
1374 after another). The code for this attribute is |
1374 after another). The code for this attribute is |
1375 *} |
1375 *} |
1376 |
1376 |
1377 ML{*fun MY_THEN thms = |
1377 ML{*fun MY_THEN thms = |
1378 Thm.rule_attribute (fn _ => fn thm => List.foldl ((op RS) o swap) thm thms)*} |
1378 Thm.rule_attribute |
|
1379 (fn _ => fn thm => fold (curry ((op RS) o swap)) thms thm)*} |
1379 |
1380 |
1380 text {* |
1381 text {* |
1381 where @{ML swap} swaps the components of a pair. The setup of this theorem |
1382 where @{ML swap} swaps the components of a pair. The setup of this theorem |
1382 attribute uses the parser @{ML thms in Attrib}, which parses a list of |
1383 attribute uses the parser @{ML thms in Attrib}, which parses a list of |
1383 theorems. |
1384 theorems. |