| changeset 27691 | ce171cbd4b93 |
| parent 25364 | 7f012f56efa3 |
| child 28819 | daca685d7bb7 |
| 27690:24738db98d34 | 27691:ce171cbd4b93 |
|---|---|
669 |
669 |
670 *} |
670 *} |
671 |
671 |
672 setup {* |
672 setup {* |
673 Theory.add_consts_i const_decls |
673 Theory.add_consts_i const_decls |
674 #> (fn thy => let val ([thm],thy') = PureThy.add_axioms_i [(("dist_axiom",dist),[])] thy |
674 #> (fn thy => let val ([thm],thy') = PureThy.add_axioms [(("dist_axiom",dist),[])] thy |
675 in (da := thm; thy') end) |
675 in (da := thm; thy') end) |
676 *} |
676 *} |
677 |
677 |
678 |
678 |
679 ML {* |
679 ML {* |