840 You can also refer to the current simpset via an antiquotation. To illustrate |
840 You can also refer to the current simpset via an antiquotation. To illustrate |
841 this we implement the function that extracts the theorem names stored in a |
841 this we implement the function that extracts the theorem names stored in a |
842 simpset. |
842 simpset. |
843 *} |
843 *} |
844 |
844 |
845 ML %grayML{*fun get_thm_names_from_ss simpset = |
845 ML %grayML{*fun get_thm_names_from_ss ctxt = |
846 let |
846 let |
|
847 val simpset = Raw_Simplifier.simpset_of ctxt |
847 val {simps,...} = Raw_Simplifier.dest_ss simpset |
848 val {simps,...} = Raw_Simplifier.dest_ss simpset |
848 in |
849 in |
849 map #1 simps |
850 map #1 simps |
850 end*} |
851 end*} |
851 |
852 |
852 text {* |
853 text {* |
853 The function @{ML_ind dest_ss in Raw_Simplifier} returns a record containing all |
854 The function @{ML_ind dest_ss in Raw_Simplifier} returns a record containing all |
854 information stored in the simpset, but here we are only interested in the names of the |
855 information stored in the simpset, but here we are only interested in the names of the |
855 simp-rules. Now you can feed in the current simpset into this function. |
856 simp-rules. Now you can feed in the current simpset into this function. |
856 The current simpset can be referred to using the antiquotation @{text "@{simpset}"}. |
857 The current simpset can be referred to using @{ML_ind simpset_of in Raw_Simplifier}. |
857 |
858 |
858 @{ML_response_fake [display,gray] |
859 @{ML_response_fake [display,gray] |
859 "get_thm_names_from_ss @{simpset}" |
860 "get_thm_names_from_ss @{context}" |
860 "[\"Nat.of_nat_eq_id\", \"Int.of_int_eq_id\", \"Nat.One_nat_def\", \<dots>]"} |
861 "[\"Nat.of_nat_eq_id\", \"Int.of_int_eq_id\", \"Nat.One_nat_def\", \<dots>]"} |
861 |
862 |
862 Again, this way of referencing simpsets makes you independent from additions |
863 Again, this way of referencing simpsets makes you independent from additions |
863 of lemmas to the simpset by the user, which can potentially cause loops in your |
864 of lemmas to the simpset by the user, which can potentially cause loops in your |
864 code. |
865 code. |