equal
deleted
inserted
replaced
1549 *} |
1549 *} |
1550 |
1550 |
1551 ML{*val my_thms = ref ([] : thm list)*} |
1551 ML{*val my_thms = ref ([] : thm list)*} |
1552 |
1552 |
1553 text {* |
1553 text {* |
1554 The purpose of this reference is that we are going to add and delete theorems |
1554 The purpose of this reference is to store a list of theorems. |
1555 to the referenced list. However, a word of warning: such references must not |
1555 We are going to modify it by adding and deleting theorems. |
|
1556 However, a word of warning: such references must not |
1556 be used in any code that is meant to be more than just for testing purposes! |
1557 be used in any code that is meant to be more than just for testing purposes! |
1557 Here it is only used to illustrate matters. We will show later how to store |
1558 Here it is only used to illustrate matters. We will show later how to store |
1558 data properly without using references. |
1559 data properly without using references. |
1559 |
1560 |
1560 We need to provide two functions that add and delete theorems from this list. |
1561 We need to provide two functions that add and delete theorems from this list. |