diff -r 26c3a9c92e11 -r a97ec0954c50 src/Pure/ex/Alternative_Headings_Examples.thy --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/Pure/ex/Alternative_Headings_Examples.thy Tue Nov 23 21:02:13 2021 +0100 @@ -0,0 +1,23 @@ +(* Title: Pure/ex/Alternative_Headings_Examples.thy + Author: Makarius +*) + +chapter \Some examples of alternative document headings\ + +theory Alternative_Headings_Examples + imports Alternative_Headings +begin + +section \Regular section\ + +subsection \Regular subsection\ + +subsubsection \Regular subsubsection\ + +subsubsection* \Alternative subsubsection\ + +subsection* \Alternative subsection\ + +section* \Alternative section\ + +end