equal
deleted
inserted
replaced
998 current simpset. For these applications, you can use @{ML_ind declaration_attribute in Thm}. |
998 current simpset. For these applications, you can use @{ML_ind declaration_attribute in Thm}. |
999 To illustrate this function, let us introduce a reference containing a list |
999 To illustrate this function, let us introduce a reference containing a list |
1000 of theorems. |
1000 of theorems. |
1001 *} |
1001 *} |
1002 |
1002 |
1003 ML{*val my_thms = ref ([] : thm list)*} |
1003 ML{*val my_thms = Unsynchronized.ref ([] : thm list)*} |
1004 |
1004 |
1005 text {* |
1005 text {* |
1006 The purpose of this reference is to store a list of theorems. |
1006 The purpose of this reference is to store a list of theorems. |
1007 We are going to modify it by adding and deleting theorems. |
1007 We are going to modify it by adding and deleting theorems. |
1008 However, a word of warning: such references must not |
1008 However, a word of warning: such references must not |