changeset 58889 | 5b7a9633cfa8 |
parent 58310 | 91ea607a34d8 |
child 60310 | 932221b62e89 |
--- a/src/HOL/Nitpick_Examples/Manual_Nits.thy Sun Nov 02 18:21:14 2014 +0100 +++ b/src/HOL/Nitpick_Examples/Manual_Nits.thy Sun Nov 02 18:21:45 2014 +0100 @@ -5,7 +5,7 @@ Examples from the Nitpick manual. *) -header {* Examples from the Nitpick Manual *} +section {* Examples from the Nitpick Manual *} (* The "expect" arguments to Nitpick in this theory and the other example theories are there so that the example can also serve as a regression test