# HG changeset patch # User wenzelm # Date 1697969903 -7200 # Node ID 1829ba610c36f430b2312fdaff2a63d4efc51d3d # Parent d769a183d51dec02ff1d06b7f0d322ba04d6dccd proper morphism; diff -r d769a183d51d -r 1829ba610c36 NEWS --- 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 \ - \<^simproc_setup>\foo (x) = \fn _ => fn _ => fn _ => SOME @{thm eq}\ + \<^simproc_setup>\foo (x) = + \fn phi => fn _ => fn _ => SOME (Morphism.thm phi @{thm eq})\ identifier test_axioms\ \