| changeset 63167 | 0909deb8059b |
| parent 61076 | bdc1e2f0a86a |
| child 74641 | 6f801e1073fa |
--- a/src/HOL/Nitpick_Examples/Special_Nits.thy Thu May 26 16:57:14 2016 +0200 +++ b/src/HOL/Nitpick_Examples/Special_Nits.thy Thu May 26 17:51:22 2016 +0200 @@ -5,7 +5,7 @@ Examples featuring Nitpick's "specialize" optimization. *) -section {* Examples Featuring Nitpick's \textit{specialize} Optimization *} +section \<open>Examples Featuring Nitpick's \textit{specialize} Optimization\<close> theory Special_Nits imports Main