| changeset 78813 | 1829ba610c36 |
| parent 78812 | d769a183d51d |
| child 78815 | 9d44cc361f19 |
--- a/NEWS Sat Oct 21 21:19:02 2023 +0200 +++ b/NEWS Sun Oct 22 12:18:23 2023 +0200 @@ -50,7 +50,8 @@ begin ML \<open> - \<^simproc_setup>\<open>foo (x) = \<open>fn _ => fn _ => fn _ => SOME @{thm eq}\<close> + \<^simproc_setup>\<open>foo (x) = + \<open>fn phi => fn _ => fn _ => SOME (Morphism.thm phi @{thm eq})\<close> identifier test_axioms\<close> \<close>