src/HOL/Examples/Rewrite_Examples.thy

     ]
   val to = NONE
   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>
   val (x, ctxt) = yield_singleton Variable.add_fixes "x" \<^context>
   val pat = [