equal
deleted
inserted
replaced
756 in |
756 in |
757 map #1 simps |
757 map #1 simps |
758 end*} |
758 end*} |
759 |
759 |
760 text {* |
760 text {* |
761 The function @{ML_ind dest_ss in MetaSimplifier} returns a record containing all |
761 The function @{ML_ind dest_ss in MetaSimplifier} returns a record containing all |
762 information stored in the simpset, but we are only interested in the names of the |
762 information stored in the simpset, but we are only interested in the names of the |
763 simp-rules. Now you can feed in the current simpset into this function. |
763 simp-rules. Now you can feed in the current simpset into this function. |
764 The current simpset can be referred to using the antiquotation @{text "@{simpset}"}. |
764 The current simpset can be referred to using the antiquotation @{text "@{simpset}"}. |
765 |
765 |
766 @{ML_response_fake [display,gray] |
766 @{ML_response_fake [display,gray] |