| changeset 74889 | 7dbac7d3cdab |
| parent 74888 | 1c50ddcf6a01 |
| child 76007 | 08288b406005 |
--- a/src/HOL/Examples/Rewrite_Examples.thy Thu Dec 09 08:32:29 2021 +0100 +++ b/src/HOL/Examples/Rewrite_Examples.thy Thu Dec 09 09:40:15 2021 +0100 @@ -268,7 +268,7 @@ val th = Rewrite.rewrite_conv ctxt (pat, to) @{thms add.commute} ct \<close> -section \<open>Regression tests\<close> +text \<open>Some regression tests\<close> ML \<open> val ct = \<^cterm>\<open>(\<lambda>b :: int. (\<lambda>a. b + a))\<close>